Metamath Proof Explorer

Theorem dochexmidlem6

Description: Lemma for dochexmid . (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dochexmidlem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochexmidlem1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochexmidlem1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochexmidlem1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochexmidlem1.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
dochexmidlem1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dochexmidlem1.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dochexmidlem1.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dochexmidlem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochexmidlem1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
dochexmidlem6.pp ⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
dochexmidlem6.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochexmidlem6.m ⊢ 𝑀 = ( 𝑋 ⊕ 𝑝 )
dochexmidlem6.xn ⊢ ( 𝜑 → 𝑋 ≠ { 0 } )
dochexmidlem6.c ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
dochexmidlem6.pl ⊢ ( 𝜑 → ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
Assertion dochexmidlem6 ( 𝜑 → 𝑀 = 𝑋 )

Proof

Step Hyp Ref Expression
1 dochexmidlem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochexmidlem1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochexmidlem1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochexmidlem1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochexmidlem1.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6 dochexmidlem1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7 dochexmidlem1.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
8 dochexmidlem1.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9 dochexmidlem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 dochexmidlem1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
11 dochexmidlem6.pp ⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
12 dochexmidlem6.z ⊢ 0 = ( 0g ‘ 𝑈 )
13 dochexmidlem6.m ⊢ 𝑀 = ( 𝑋 ⊕ 𝑝 )
14 dochexmidlem6.xn ⊢ ( 𝜑 → 𝑋 ≠ { 0 } )
15 dochexmidlem6.c ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
16 dochexmidlem6.pl ⊢ ( 𝜑 → ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 16 dochexmidlem5 ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) = { 0 } )
18 17 fveq2d ⊢ ( 𝜑 → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ) = ( ⊥ ‘ { 0 } ) )
19 1 3 2 4 12 doch0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ { 0 } ) = 𝑉 )
20 9 19 syl ⊢ ( 𝜑 → ( ⊥ ‘ { 0 } ) = 𝑉 )
21 18 20 eqtrd ⊢ ( 𝜑 → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ) = 𝑉 )
22 21 ineq1d ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ) ∩ 𝑀 ) = ( 𝑉 ∩ 𝑀 ) )
23 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
24 4 5 lssss ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ⊆ 𝑉 )
25 10 24 syl ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
26 1 3 4 2 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
27 9 25 26 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
28 1 23 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
29 9 27 28 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
30 15 29 eqeltrrd ⊢ ( 𝜑 → 𝑋 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
31 1 23 3 7 8 9 30 11 dihsmatrn ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑝 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
32 13 31 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
33 1 3 23 5 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑀 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑀 ∈ 𝑆 )
34 9 32 33 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ 𝑆 )
35 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
36 5 8 35 11 lsatlssel ⊢ ( 𝜑 → 𝑝 ∈ 𝑆 )
37 5 7 lsmcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ 𝑝 ∈ 𝑆 ) → ( 𝑋 ⊕ 𝑝 ) ∈ 𝑆 )
38 35 10 36 37 syl3anc ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑝 ) ∈ 𝑆 )
39 4 5 lssss ⊢ ( ( 𝑋 ⊕ 𝑝 ) ∈ 𝑆 → ( 𝑋 ⊕ 𝑝 ) ⊆ 𝑉 )
40 38 39 syl ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑝 ) ⊆ 𝑉 )
41 13 40 eqsstrid ⊢ ( 𝜑 → 𝑀 ⊆ 𝑉 )
42 1 23 3 4 2 9 41 dochoccl ⊢ ( 𝜑 → ( 𝑀 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑀 ) ) = 𝑀 ) )
43 32 42 mpbid ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑀 ) ) = 𝑀 )
44 5 lsssssubg ⊢ ( 𝑈 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
45 35 44 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
46 45 10 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( SubGrp ‘ 𝑈 ) )
47 45 36 sseldd ⊢ ( 𝜑 → 𝑝 ∈ ( SubGrp ‘ 𝑈 ) )
48 7 lsmub1 ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) ∧ 𝑝 ∈ ( SubGrp ‘ 𝑈 ) ) → 𝑋 ⊆ ( 𝑋 ⊕ 𝑝 ) )
49 46 47 48 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ ( 𝑋 ⊕ 𝑝 ) )
50 49 13 sseqtrrdi ⊢ ( 𝜑 → 𝑋 ⊆ 𝑀 )
51 1 3 5 2 9 10 34 43 50 dihoml4 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ) ∩ 𝑀 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
52 sseqin2 ⊢ ( 𝑀 ⊆ 𝑉 ↔ ( 𝑉 ∩ 𝑀 ) = 𝑀 )
53 41 52 sylib ⊢ ( 𝜑 → ( 𝑉 ∩ 𝑀 ) = 𝑀 )
54 22 51 53 3eqtr3rd ⊢ ( 𝜑 → 𝑀 = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
55 54 15 eqtrd ⊢ ( 𝜑 → 𝑀 = 𝑋 )