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 
|- V = ( Base ` W )
lsmcv.s 
|- S = ( LSubSp ` W )
lsmcv.n 
|- N = ( LSpan ` W )
lsmcv.p 
|- .(+) = ( LSSum ` W )
lsmcv.w 
|- ( ph -> W e. LVec )
lsmcv.t 
|- ( ph -> T e. S )
lsmcv.u 
|- ( ph -> U e. S )
lsmcv.x 
|- ( ph -> X e. V )
Assertion lsmcv 
|- ( ( ph /\ T C. U /\ U C_ ( T .(+) ( N ` { X } ) ) ) -> U = ( T .(+) ( N ` { X } ) ) )

Proof

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