This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmapjat2

Description: The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012)

Ref Expression
Hypotheses pmapjat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapjat.j ⊢ ∨ = ( join ‘ 𝐾 )
pmapjat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pmapjat.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
pmapjat.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion pmapjat2 ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( 𝑄 ∨ 𝑋 ) ) = ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 pmapjat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapjat.j ⊢ ∨ = ( join ‘ 𝐾 )
3 pmapjat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 pmapjat.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
5 pmapjat.p ⊢ + = ( +𝑃 ‘ 𝐾 )
6 1 2 3 4 5 pmapjat1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )
7 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
8 7 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ Lat )
9 1 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
10 9 3ad2ant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ 𝐵 )
11 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
12 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑄 ∨ 𝑋 ) = ( 𝑋 ∨ 𝑄 ) )
13 8 10 11 12 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑋 ) = ( 𝑋 ∨ 𝑄 ) )
14 13 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( 𝑄 ∨ 𝑋 ) ) = ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) )
15 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ HL )
16 1 3 4 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 )
17 15 10 16 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 )
18 1 3 4 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 )
19 18 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 )
20 3 5 paddcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 ∧ ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 ) → ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑋 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )
21 8 17 19 20 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑋 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )
22 6 14 21 3eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( 𝑄 ∨ 𝑋 ) ) = ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑋 ) ) )