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

Metamath Proof Explorer

Theorem lsmcv

Description: Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of Kalmbach p. 153. ( spansncvi analog.) TODO: ugly proof; can it be shortened? (Contributed by NM, 2-Oct-2014)

Ref Expression
Hypotheses lsmcv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsmcv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsmcv.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsmcv.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsmcv.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsmcv.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lsmcv.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lsmcv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion lsmcv ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑈 = ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )

Proof

Step Hyp Ref Expression
1 lsmcv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsmcv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lsmcv.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lsmcv.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
5 lsmcv.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lsmcv.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
7 lsmcv.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
8 lsmcv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 simp3 ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
10 simp2 ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑇 ⊊ 𝑈 )
11 pssss ⊢ ( 𝑇 ⊊ 𝑈 → 𝑇 ⊆ 𝑈 )
12 10 11 syl ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑇 ⊆ 𝑈 )
13 pssnel ⊢ ( 𝑇 ⊊ 𝑈 → ∃ 𝑥 ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) )
14 10 13 syl ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) )
15 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
16 simprl ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → 𝑥 ∈ 𝑈 )
17 15 16 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → 𝑥 ∈ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
18 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
19 5 18 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
20 2 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
21 19 20 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
22 21 6 sseldd ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
23 1 2 3 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
24 19 8 23 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
25 21 24 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
26 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
27 26 4 lsmelval ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑥 ∈ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
28 22 25 27 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
29 28 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑥 ∈ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → ( 𝑥 ∈ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
31 17 30 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) )
32 simp1rr ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ¬ 𝑥 ∈ 𝑇 )
33 simp2l ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑦 ∈ 𝑇 )
34 oveq2 ⊢ ( 𝑧 = ( 0g ‘ 𝑊 ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) )
35 34 eqeq2d ⊢ ( 𝑧 = ( 0g ‘ 𝑊 ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ↔ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ) )
36 35 biimpac ⊢ ( ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∧ 𝑧 = ( 0g ‘ 𝑊 ) ) → 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) )
37 19 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑊 ∈ LMod )
38 37 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑊 ∈ LMod )
39 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑇 ∈ 𝑆 )
40 39 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑇 ∈ 𝑆 )
41 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑦 ∈ 𝑇 )
42 1 2 lssel ⊢ ( ( 𝑇 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ∈ 𝑉 )
43 40 41 42 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑦 ∈ 𝑉 )
44 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
45 1 26 44 lmod0vrid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 𝑦 )
46 38 43 45 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 𝑦 )
47 46 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ↔ 𝑥 = 𝑦 ) )
48 47 biimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) → 𝑥 = 𝑦 ) )
49 48 ex ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → ( ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) → 𝑥 = 𝑦 ) ) )
50 36 49 syl7 ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → ( ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∧ 𝑧 = ( 0g ‘ 𝑊 ) ) → 𝑥 = 𝑦 ) ) )
51 50 exp4a ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → ( ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝑧 = ( 0g ‘ 𝑊 ) → 𝑥 = 𝑦 ) ) ) )
52 51 3imp ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( 𝑧 = ( 0g ‘ 𝑊 ) → 𝑥 = 𝑦 ) )
53 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑇 ↔ 𝑦 ∈ 𝑇 ) )
54 53 biimparc ⊢ ( ( 𝑦 ∈ 𝑇 ∧ 𝑥 = 𝑦 ) → 𝑥 ∈ 𝑇 )
55 33 52 54 syl6an ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( 𝑧 = ( 0g ‘ 𝑊 ) → 𝑥 ∈ 𝑇 ) )
56 55 necon3bd ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ¬ 𝑥 ∈ 𝑇 → 𝑧 ≠ ( 0g ‘ 𝑊 ) ) )
57 32 56 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑧 ≠ ( 0g ‘ 𝑊 ) )
58 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑊 ∈ LVec )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → 𝑊 ∈ LVec )
60 59 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑊 ∈ LVec )
61 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
62 18 61 syl ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ Abel )
63 60 62 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑊 ∈ Abel )
64 simp1l1 ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝜑 )
65 64 6 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑇 ∈ 𝑆 )
66 65 33 42 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑦 ∈ 𝑉 )
67 60 18 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑊 ∈ LMod )
68 64 8 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑋 ∈ 𝑉 )
69 67 68 23 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
70 simp2r ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )
71 1 2 lssel ⊢ ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑧 ∈ 𝑉 )
72 69 70 71 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑧 ∈ 𝑉 )
73 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
74 1 26 73 ablpncan2 ⊢ ( ( 𝑊 ∈ Abel ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ( -g ‘ 𝑊 ) 𝑦 ) = 𝑧 )
75 63 66 72 74 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ( -g ‘ 𝑊 ) 𝑦 ) = 𝑧 )
76 64 7 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑈 ∈ 𝑆 )
77 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) )
78 simp1rl ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑥 ∈ 𝑈 )
79 77 78 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑈 )
80 simp1l2 ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑇 ⊊ 𝑈 )
81 11 sselda ⊢ ( ( 𝑇 ⊊ 𝑈 ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ∈ 𝑈 )
82 80 33 81 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑦 ∈ 𝑈 )
83 73 2 lssvsubcl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ( -g ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 )
84 67 76 79 82 83 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ( -g ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 )
85 75 84 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑧 ∈ 𝑈 )
86 60 3ad2ant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑊 ∈ LVec )
87 64 3ad2ant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → 𝜑 )
88 87 8 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
89 simp12r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )
90 simp2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≠ ( 0g ‘ 𝑊 ) )
91 1 44 3 86 88 89 90 lspsneleq ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑧 } ) = ( 𝑁 ‘ { 𝑋 } ) )
92 86 18 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑊 ∈ LMod )
93 87 7 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
94 simp3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ 𝑈 )
95 2 3 92 93 94 ellspsn5 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑈 )
96 91 95 eqsstrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ∧ 𝑧 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
97 57 85 96 mpd3an23 ⊢ ( ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
98 97 3exp ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → ( ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )
99 98 rexlimdvv ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
100 31 99 mpd ⊢ ( ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ 𝑇 ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
101 14 100 exlimddv ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
102 21 7 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
103 4 lsmlub ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑇 ⊆ 𝑈 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ↔ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ 𝑈 ) )
104 22 25 102 103 syl3anc ⊢ ( 𝜑 → ( ( 𝑇 ⊆ 𝑈 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ↔ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ 𝑈 ) )
105 104 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( ( 𝑇 ⊆ 𝑈 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ↔ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ 𝑈 ) )
106 12 101 105 mpbi2and ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ 𝑈 )
107 9 106 eqssd ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑈 = ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )