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

Metamath Proof Explorer

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