Metamath Proof Explorer

Theorem dihmeetlem16N

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 dihmeetlem16N ( ( ( ( 𝐾 ∈ 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 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
11 1 2 3 4 5 6 7 8 9 10 dihmeetlem15N ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑟 ) ∩ ( 𝐼 ‘ 𝑝 ) ) = { ( 0g ‘ 𝑈 ) } )
12 11 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ⊕ ( ( 𝐼 ‘ 𝑟 ) ∩ ( 𝐼 ‘ 𝑝 ) ) ) = ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ⊕ { ( 0g ‘ 𝑈 ) } ) )
13 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → 𝑌 ∈ 𝐵 )
15 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → 𝑝 ∈ 𝐴 )
16 1 6 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
17 15 16 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → 𝑝 ∈ 𝐵 )
18 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) )
19 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → 𝑟 ≤ 𝑌 )
20 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 )
21 1 2 3 4 5 6 7 8 9 dihmeetlem14N ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ⊕ ( ( 𝐼 ‘ 𝑟 ) ∩ ( 𝐼 ‘ 𝑝 ) ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑝 ) ) )
22 13 14 17 18 19 20 21 syl33anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ⊕ ( ( 𝐼 ‘ 𝑟 ) ∩ ( 𝐼 ‘ 𝑝 ) ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑝 ) ) )
23 3 7 13 dvhlmod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → 𝑈 ∈ LMod )
24 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → 𝐾 ∈ HL )
25 24 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
26 1 5 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑝 ) ∈ 𝐵 )
27 25 14 17 26 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( 𝑌 ∧ 𝑝 ) ∈ 𝐵 )
28 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
29 1 3 9 7 28 dihlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∧ 𝑝 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
30 13 27 29 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
31 28 lsssubg ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
32 23 30 31 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
33 10 8 lsm01 ⊢ ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ∈ ( SubGrp ‘ 𝑈 ) → ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ⊕ { ( 0g ‘ 𝑈 ) } ) = ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) )
34 32 33 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ⊕ { ( 0g ‘ 𝑈 ) } ) = ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) )
35 12 22 34 3eqtr3rd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑝 ) ) )