Theorem pmapjlln1

Description: The projective map of the join of a lattice element and a lattice line (expressed as the join Q .\/ R of two atoms). (Contributed by NM, 16-Sep-2012)

	Ref	Expression
Hypotheses	pmapjat.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	pmapjat.j	⊢ ∨ = ( join ‘ 𝐾 )
	pmapjat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pmapjat.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
	pmapjat.p	⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion	pmapjlln1	⊢ ( ( 𝐾 ∈ 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		simpl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
7	1 3 4	pmapssat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 )
8	7	3ad2antr1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 )
9		simpr2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
10	1 3	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
11	9 10	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐵 )
12	1 3 4	pmapssat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 )
13	11 12	syldan	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 )
14		simpr3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
15	1 3	atbase	⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵 )
16	14 15	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐵 )
17	1 3 4	pmapssat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑅 ) ⊆ 𝐴 )
18	16 17	syldan	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑀 ‘ 𝑅 ) ⊆ 𝐴 )
19	3 5	paddass	⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑀 ‘ 𝑋 ) ⊆ 𝐴 ∧ ( 𝑀 ‘ 𝑄 ) ⊆ 𝐴 ∧ ( 𝑀 ‘ 𝑅 ) ⊆ 𝐴 ) ) → ( ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) + ( 𝑀 ‘ 𝑅 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑅 ) ) ) )
20	6 8 13 18 19	syl13anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) + ( 𝑀 ‘ 𝑅 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑅 ) ) ) )
21		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
22	21	adantr	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
23		simpr1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
24	1 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
25	22 23 11 24	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
26	1 2 3 4 5	pmapjat1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑀 ‘ ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑅 ) ) = ( ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) + ( 𝑀 ‘ 𝑅 ) ) )
27	6 25 14 26	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑀 ‘ ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑅 ) ) = ( ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) + ( 𝑀 ‘ 𝑅 ) ) )
28	1 2	latjass	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑋 ∨ ( 𝑄 ∨ 𝑅 ) ) )
29	22 23 11 16 28	syl13anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑋 ∨ ( 𝑄 ∨ 𝑅 ) ) )
30	29	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑀 ‘ ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑅 ) ) = ( 𝑀 ‘ ( 𝑋 ∨ ( 𝑄 ∨ 𝑅 ) ) ) )
31	1 2 3 4 5	pmapjat1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )
32	31	3adant3r3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) )
33	32	oveq1d	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑀 ‘ ( 𝑋 ∨ 𝑄 ) ) + ( 𝑀 ‘ 𝑅 ) ) = ( ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) + ( 𝑀 ‘ 𝑅 ) ) )
34	27 30 33	3eqtr3d	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ ( 𝑄 ∨ 𝑅 ) ) ) = ( ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ 𝑄 ) ) + ( 𝑀 ‘ 𝑅 ) ) )
35	1 2 3 4 5	pmapjat1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐵 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑀 ‘ ( 𝑄 ∨ 𝑅 ) ) = ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑅 ) ) )
36	6 11 14 35	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑄 ∨ 𝑅 ) ) = ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑅 ) ) )
37	36	oveq2d	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ ( 𝑄 ∨ 𝑅 ) ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( ( 𝑀 ‘ 𝑄 ) + ( 𝑀 ‘ 𝑅 ) ) ) )
38	20 34 37	3eqtr4d	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑋 ∨ ( 𝑄 ∨ 𝑅 ) ) ) = ( ( 𝑀 ‘ 𝑋 ) + ( 𝑀 ‘ ( 𝑄 ∨ 𝑅 ) ) ) )