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

Metamath Proof Explorer

Theorem dihmeetALTN

Description: Isomorphism H of a lattice meet. This version does not depend on the atomisticity of the constructed vector space. TODO: Delete? (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetALT.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihmeetALT.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihmeetALT.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihmeetALT.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihmeetALTN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 dihmeetALT.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihmeetALT.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 dihmeetALT.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihmeetALT.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝐾 ∈ HL )
6 5 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝐾 ∈ Lat )
7 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝑋 ∈ 𝐵 )
8 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝑌 ∈ 𝐵 )
9 1 2 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
10 6 7 8 9 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
11 10 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( 𝐼 ‘ ( 𝑌 ∧ 𝑋 ) ) )
12 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝑋 ( le ‘ 𝐾 ) 𝑊 )
14 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
15 1 14 2 3 4 dihmeetbN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑋 ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑋 ) ) )
16 12 8 7 13 15 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑋 ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑋 ) ) )
17 incom ⊢ ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑋 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) )
18 16 17 eqtrdi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑋 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
19 11 18 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
20 simpll1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21 simpll2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → 𝑋 ∈ 𝐵 )
22 simpll3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → 𝑌 ∈ 𝐵 )
23 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → 𝑌 ( le ‘ 𝐾 ) 𝑊 )
24 1 14 2 3 4 dihmeetbN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
25 20 21 22 23 24 syl112anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
26 25 adantlr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
27 simp1l1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
28 simp1l2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → 𝑋 ∈ 𝐵 )
29 simp1r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 )
30 simp1l3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → 𝑌 ∈ 𝐵 )
31 simp3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 )
32 30 31 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) )
33 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 )
34 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
35 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
36 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
37 eqid ⊢ ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
38 1 14 3 34 2 35 36 37 4 dihmeetlem20N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
39 27 28 29 32 33 38 syl122anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
40 39 3expa ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
41 26 40 pm2.61dan ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
42 simpll1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
43 simpll2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) → 𝑋 ∈ 𝐵 )
44 simpll3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) → 𝑌 ∈ 𝐵 )
45 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) → ¬ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 )
46 1 14 2 3 4 dihmeetcN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
47 42 43 44 45 46 syl121anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
48 41 47 pm2.61dan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
49 19 48 pm2.61dan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )