Metamath Proof Explorer

Theorem dihmeetlem19N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem14.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihmeetlem14.l ⊢ ≤ = ( le ‘ 𝐾 )
dihmeetlem14.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihmeetlem14.j ⊢ ∨ = ( join ‘ 𝐾 )
dihmeetlem14.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihmeetlem14.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihmeetlem14.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem14.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dihmeetlem14.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihmeetlem19N ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 dihmeetlem14.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihmeetlem14.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihmeetlem14.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihmeetlem14.j ⊢ ∨ = ( join ‘ 𝐾 )
5 dihmeetlem14.m ⊢ ∧ = ( meet ‘ 𝐾 )
6 dihmeetlem14.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 dihmeetlem14.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 dihmeetlem14.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
9 dihmeetlem14.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
10 incom ⊢ ( ( 𝐼 ‘ 𝑝 ) ∩ ( 𝐼 ‘ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑝 ) )
11 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
12 1 2 3 4 5 6 7 8 9 11 dihmeetlem18N ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑝 ) ) = { ( 0g ‘ 𝑈 ) } )
13 10 12 syl5eq ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( ( 𝐼 ‘ 𝑝 ) ∩ ( 𝐼 ‘ 𝑌 ) ) = { ( 0g ‘ 𝑈 ) } )
14 13 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊕ ( ( 𝐼 ‘ 𝑝 ) ∩ ( 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊕ { ( 0g ‘ 𝑈 ) } ) )
15 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → 𝑋 ∈ 𝐵 )
17 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → 𝑌 ∈ 𝐵 )
18 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) )
19 simpr31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → 𝑝 ≤ 𝑋 )
20 simpr33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 )
21 1 2 3 4 5 6 7 8 9 dihmeetlem12N ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑝 ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊕ ( ( 𝐼 ‘ 𝑝 ) ∩ ( 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
22 15 16 17 18 19 20 21 syl33anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊕ ( ( 𝐼 ‘ 𝑝 ) ∩ ( 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
23 3 7 15 dvhlmod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → 𝑈 ∈ LMod )
24 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → 𝐾 ∈ HL )
25 24 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → 𝐾 ∈ Lat )
26 1 5 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
27 25 16 17 26 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
28 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
29 1 3 9 7 28 dihlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
30 15 27 29 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
31 28 lsssubg ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
32 23 30 31 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
33 11 8 lsm01 ⊢ ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ∈ ( SubGrp ‘ 𝑈 ) → ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊕ { ( 0g ‘ 𝑈 ) } ) = ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) )
34 32 33 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊕ { ( 0g ‘ 𝑈 ) } ) = ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) )
35 14 22 34 3eqtr3rd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )