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 ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝐼 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝐼𝑋 ) ∩ ( 𝐼𝑌 ) ) )