# 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 lspsnel5a ( ( ( ( ( 𝜑𝑇𝑈𝑈 ⊆ ( 𝑇 ( 𝑁 ‘ { 𝑋 } ) ) ) ∧ ( 𝑥𝑈 ∧ ¬ 𝑥𝑇 ) ) ∧ ( 𝑦𝑇𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) ∧ 𝑥 = ( 𝑦 ( +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 ( ( 𝜑𝑇𝑈𝑈 ⊆ ( 𝑇 ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑈 = ( 𝑇 ( 𝑁 ‘ { 𝑋 } ) ) )