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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( 𝑄 ∨ 𝑋 ) ) = ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑋 ) ) )