Metamath Proof Explorer

Theorem frgpnabllem1

Description: Lemma for frgpnabl . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 25-Apr-2024)

Ref Expression
Hypotheses frgpnabl.g 
|- G = ( freeGrp ` I )
frgpnabl.w 
|- W = ( _I ` Word ( I X. 2o ) )
frgpnabl.r 
|- .~ = ( ~FG ` I )
frgpnabl.p 
|- .+ = ( +g ` G )
frgpnabl.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
frgpnabl.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
frgpnabl.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
frgpnabl.u 
|- U = ( varFGrp ` I )
frgpnabl.i 
|- ( ph -> I e. V )
frgpnabl.a 
|- ( ph -> A e. I )
frgpnabl.b 
|- ( ph -> B e. I )
Assertion frgpnabllem1 
|- ( ph -> <" <. A , (/) >. <. B , (/) >. "> e. ( D i^i ( ( U ` A ) .+ ( U ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 frgpnabl.g 
 |-  G = ( freeGrp ` I )
2 frgpnabl.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
3 frgpnabl.r 
 |-  .~ = ( ~FG ` I )
4 frgpnabl.p 
 |-  .+ = ( +g ` G )
5 frgpnabl.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
6 frgpnabl.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
7 frgpnabl.d 
 |-  D = ( W \ U_ x e. W ran ( T ` x ) )
8 frgpnabl.u 
 |-  U = ( varFGrp ` I )
9 frgpnabl.i 
 |-  ( ph -> I e. V )
10 frgpnabl.a 
 |-  ( ph -> A e. I )
11 frgpnabl.b 
 |-  ( ph -> B e. I )
12 0ex 
 |-  (/) e. _V
13 12 prid1 
 |-  (/) e. { (/) , 1o }
14 df2o3 
 |-  2o = { (/) , 1o }
15 13 14 eleqtrri 
 |-  (/) e. 2o
16 opelxpi 
 |-  ( ( A e. I /\ (/) e. 2o ) -> <. A , (/) >. e. ( I X. 2o ) )
17 10 15 16 sylancl 
 |-  ( ph -> <. A , (/) >. e. ( I X. 2o ) )
18 opelxpi 
 |-  ( ( B e. I /\ (/) e. 2o ) -> <. B , (/) >. e. ( I X. 2o ) )
19 11 15 18 sylancl 
 |-  ( ph -> <. B , (/) >. e. ( I X. 2o ) )
20 17 19 s2cld 
 |-  ( ph -> <" <. A , (/) >. <. B , (/) >. "> e. Word ( I X. 2o ) )
21 2on 
 |-  2o e. On
22 xpexg 
 |-  ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
23 9 21 22 sylancl 
 |-  ( ph -> ( I X. 2o ) e. _V )
24 wrdexg 
 |-  ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V )
25 fvi 
 |-  ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
26 23 24 25 3syl 
 |-  ( ph -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
27 2 26 eqtrid 
 |-  ( ph -> W = Word ( I X. 2o ) )
28 20 27 eleqtrrd 
 |-  ( ph -> <" <. A , (/) >. <. B , (/) >. "> e. W )
29 1n0 
 |-  1o =/= (/)
30 2cn 
 |-  2 e. CC
31 30 addlidi 
 |-  ( 0 + 2 ) = 2
32 s2len 
 |-  ( # ` <" <. A , (/) >. <. B , (/) >. "> ) = 2
33 31 32 eqtr4i 
 |-  ( 0 + 2 ) = ( # ` <" <. A , (/) >. <. B , (/) >. "> )
34 2 3 5 6 efgtlen 
 |-  ( ( x e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) -> ( # ` <" <. A , (/) >. <. B , (/) >. "> ) = ( ( # ` x ) + 2 ) )
35 34 adantll 
 |-  ( ( ( ph /\ x e. W ) /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) -> ( # ` <" <. A , (/) >. <. B , (/) >. "> ) = ( ( # ` x ) + 2 ) )
36 33 35 eqtrid 
 |-  ( ( ( ph /\ x e. W ) /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) -> ( 0 + 2 ) = ( ( # ` x ) + 2 ) )
37 36 ex 
 |-  ( ( ph /\ x e. W ) -> ( <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) -> ( 0 + 2 ) = ( ( # ` x ) + 2 ) ) )
38 0cnd 
 |-  ( ( ph /\ x e. W ) -> 0 e. CC )
39 simpr 
 |-  ( ( ph /\ x e. W ) -> x e. W )
40 2 efgrcl 
 |-  ( x e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
41 40 simprd 
 |-  ( x e. W -> W = Word ( I X. 2o ) )
42 41 adantl 
 |-  ( ( ph /\ x e. W ) -> W = Word ( I X. 2o ) )
43 39 42 eleqtrd 
 |-  ( ( ph /\ x e. W ) -> x e. Word ( I X. 2o ) )
44 lencl 
 |-  ( x e. Word ( I X. 2o ) -> ( # ` x ) e. NN0 )
45 43 44 syl 
 |-  ( ( ph /\ x e. W ) -> ( # ` x ) e. NN0 )
46 45 nn0cnd 
 |-  ( ( ph /\ x e. W ) -> ( # ` x ) e. CC )
47 2cnd 
 |-  ( ( ph /\ x e. W ) -> 2 e. CC )
48 38 46 47 addcan2d 
 |-  ( ( ph /\ x e. W ) -> ( ( 0 + 2 ) = ( ( # ` x ) + 2 ) <-> 0 = ( # ` x ) ) )
49 37 48 sylibd 
 |-  ( ( ph /\ x e. W ) -> ( <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) -> 0 = ( # ` x ) ) )
50 2 3 5 6 efgtf 
 |-  ( (/) e. W -> ( ( T ` (/) ) = ( a e. ( 0 ... ( # ` (/) ) ) , b e. ( I X. 2o ) |-> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` (/) ) : ( ( 0 ... ( # ` (/) ) ) X. ( I X. 2o ) ) --> W ) )
51 50 adantl 
 |-  ( ( ph /\ (/) e. W ) -> ( ( T ` (/) ) = ( a e. ( 0 ... ( # ` (/) ) ) , b e. ( I X. 2o ) |-> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` (/) ) : ( ( 0 ... ( # ` (/) ) ) X. ( I X. 2o ) ) --> W ) )
52 51 simpld 
 |-  ( ( ph /\ (/) e. W ) -> ( T ` (/) ) = ( a e. ( 0 ... ( # ` (/) ) ) , b e. ( I X. 2o ) |-> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) ) )
53 52 rneqd 
 |-  ( ( ph /\ (/) e. W ) -> ran ( T ` (/) ) = ran ( a e. ( 0 ... ( # ` (/) ) ) , b e. ( I X. 2o ) |-> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) ) )
54 53 eleq2d 
 |-  ( ( ph /\ (/) e. W ) -> ( <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` (/) ) <-> <" <. A , (/) >. <. B , (/) >. "> e. ran ( a e. ( 0 ... ( # ` (/) ) ) , b e. ( I X. 2o ) |-> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) ) ) )
55 eqid 
 |-  ( a e. ( 0 ... ( # ` (/) ) ) , b e. ( I X. 2o ) |-> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) ) = ( a e. ( 0 ... ( # ` (/) ) ) , b e. ( I X. 2o ) |-> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) )
56 ovex 
 |-  ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) e. _V
57 55 56 elrnmpo 
 |-  ( <" <. A , (/) >. <. B , (/) >. "> e. ran ( a e. ( 0 ... ( # ` (/) ) ) , b e. ( I X. 2o ) |-> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) ) <-> E. a e. ( 0 ... ( # ` (/) ) ) E. b e. ( I X. 2o ) <" <. A , (/) >. <. B , (/) >. "> = ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) )
58 wrd0 
 |-  (/) e. Word ( I X. 2o )
59 58 a1i 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> (/) e. Word ( I X. 2o ) )
60 simprr 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> b e. ( I X. 2o ) )
61 5 efgmf 
 |-  M : ( I X. 2o ) --> ( I X. 2o )
62 61 ffvelcdmi 
 |-  ( b e. ( I X. 2o ) -> ( M ` b ) e. ( I X. 2o ) )
63 60 62 syl 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> ( M ` b ) e. ( I X. 2o ) )
64 60 63 s2cld 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> <" b ( M ` b ) "> e. Word ( I X. 2o ) )
65 ccatidid 
 |-  ( (/) ++ (/) ) = (/)
66 65 oveq1i 
 |-  ( ( (/) ++ (/) ) ++ (/) ) = ( (/) ++ (/) )
67 66 65 eqtr2i 
 |-  (/) = ( ( (/) ++ (/) ) ++ (/) )
68 67 a1i 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> (/) = ( ( (/) ++ (/) ) ++ (/) ) )
69 simprl 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> a e. ( 0 ... ( # ` (/) ) ) )
70 hash0 
 |-  ( # ` (/) ) = 0
71 70 oveq2i 
 |-  ( 0 ... ( # ` (/) ) ) = ( 0 ... 0 )
72 69 71 eleqtrdi 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> a e. ( 0 ... 0 ) )
73 elfz1eq 
 |-  ( a e. ( 0 ... 0 ) -> a = 0 )
74 72 73 syl 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> a = 0 )
75 74 70 eqtr4di 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> a = ( # ` (/) ) )
76 70 oveq2i 
 |-  ( a + ( # ` (/) ) ) = ( a + 0 )
77 0cn 
 |-  0 e. CC
78 74 77 eqeltrdi 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> a e. CC )
79 78 addridd 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> ( a + 0 ) = a )
80 76 79 eqtr2id 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> a = ( a + ( # ` (/) ) ) )
81 59 59 59 64 68 75 80 splval2 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) = ( ( (/) ++ <" b ( M ` b ) "> ) ++ (/) ) )
82 ccatlid 
 |-  ( <" b ( M ` b ) "> e. Word ( I X. 2o ) -> ( (/) ++ <" b ( M ` b ) "> ) = <" b ( M ` b ) "> )
83 82 oveq1d 
 |-  ( <" b ( M ` b ) "> e. Word ( I X. 2o ) -> ( ( (/) ++ <" b ( M ` b ) "> ) ++ (/) ) = ( <" b ( M ` b ) "> ++ (/) ) )
84 ccatrid 
 |-  ( <" b ( M ` b ) "> e. Word ( I X. 2o ) -> ( <" b ( M ` b ) "> ++ (/) ) = <" b ( M ` b ) "> )
85 83 84 eqtrd 
 |-  ( <" b ( M ` b ) "> e. Word ( I X. 2o ) -> ( ( (/) ++ <" b ( M ` b ) "> ) ++ (/) ) = <" b ( M ` b ) "> )
86 64 85 syl 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> ( ( (/) ++ <" b ( M ` b ) "> ) ++ (/) ) = <" b ( M ` b ) "> )
87 81 86 eqtrd 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) = <" b ( M ` b ) "> )
88 87 eqeq2d 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> ( <" <. A , (/) >. <. B , (/) >. "> = ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) <-> <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) )
89 10 ad3antrrr 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> A e. I )
90 1on 
 |-  1o e. On
91 90 a1i 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> 1o e. On )
92 simpr 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> )
93 92 fveq1d 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> ( <" <. A , (/) >. <. B , (/) >. "> ` 1 ) = ( <" b ( M ` b ) "> ` 1 ) )
94 opex 
 |-  <. B , (/) >. e. _V
95 s2fv1 
 |-  ( <. B , (/) >. e. _V -> ( <" <. A , (/) >. <. B , (/) >. "> ` 1 ) = <. B , (/) >. )
96 94 95 ax-mp 
 |-  ( <" <. A , (/) >. <. B , (/) >. "> ` 1 ) = <. B , (/) >.
97 fvex 
 |-  ( M ` b ) e. _V
98 s2fv1 
 |-  ( ( M ` b ) e. _V -> ( <" b ( M ` b ) "> ` 1 ) = ( M ` b ) )
99 97 98 ax-mp 
 |-  ( <" b ( M ` b ) "> ` 1 ) = ( M ` b )
100 93 96 99 3eqtr3g 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> <. B , (/) >. = ( M ` b ) )
101 92 fveq1d 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> ( <" <. A , (/) >. <. B , (/) >. "> ` 0 ) = ( <" b ( M ` b ) "> ` 0 ) )
102 opex 
 |-  <. A , (/) >. e. _V
103 s2fv0 
 |-  ( <. A , (/) >. e. _V -> ( <" <. A , (/) >. <. B , (/) >. "> ` 0 ) = <. A , (/) >. )
104 102 103 ax-mp 
 |-  ( <" <. A , (/) >. <. B , (/) >. "> ` 0 ) = <. A , (/) >.
105 s2fv0 
 |-  ( b e. _V -> ( <" b ( M ` b ) "> ` 0 ) = b )
106 105 elv 
 |-  ( <" b ( M ` b ) "> ` 0 ) = b
107 101 104 106 3eqtr3g 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> <. A , (/) >. = b )
108 107 fveq2d 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> ( M ` <. A , (/) >. ) = ( M ` b ) )
109 5 efgmval 
 |-  ( ( A e. I /\ (/) e. 2o ) -> ( A M (/) ) = <. A , ( 1o \ (/) ) >. )
110 89 15 109 sylancl 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> ( A M (/) ) = <. A , ( 1o \ (/) ) >. )
111 df-ov 
 |-  ( A M (/) ) = ( M ` <. A , (/) >. )
112 dif0 
 |-  ( 1o \ (/) ) = 1o
113 112 opeq2i 
 |-  <. A , ( 1o \ (/) ) >. = <. A , 1o >.
114 110 111 113 3eqtr3g 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> ( M ` <. A , (/) >. ) = <. A , 1o >. )
115 100 108 114 3eqtr2rd 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> <. A , 1o >. = <. B , (/) >. )
116 opthg 
 |-  ( ( A e. I /\ 1o e. On ) -> ( <. A , 1o >. = <. B , (/) >. <-> ( A = B /\ 1o = (/) ) ) )
117 116 simplbda 
 |-  ( ( ( A e. I /\ 1o e. On ) /\ <. A , 1o >. = <. B , (/) >. ) -> 1o = (/) )
118 89 91 115 117 syl21anc 
 |-  ( ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) /\ <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> ) -> 1o = (/) )
119 118 ex 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> ( <" <. A , (/) >. <. B , (/) >. "> = <" b ( M ` b ) "> -> 1o = (/) ) )
120 88 119 sylbid 
 |-  ( ( ( ph /\ (/) e. W ) /\ ( a e. ( 0 ... ( # ` (/) ) ) /\ b e. ( I X. 2o ) ) ) -> ( <" <. A , (/) >. <. B , (/) >. "> = ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) -> 1o = (/) ) )
121 120 rexlimdvva 
 |-  ( ( ph /\ (/) e. W ) -> ( E. a e. ( 0 ... ( # ` (/) ) ) E. b e. ( I X. 2o ) <" <. A , (/) >. <. B , (/) >. "> = ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) -> 1o = (/) ) )
122 57 121 biimtrid 
 |-  ( ( ph /\ (/) e. W ) -> ( <" <. A , (/) >. <. B , (/) >. "> e. ran ( a e. ( 0 ... ( # ` (/) ) ) , b e. ( I X. 2o ) |-> ( (/) splice <. a , a , <" b ( M ` b ) "> >. ) ) -> 1o = (/) ) )
123 54 122 sylbid 
 |-  ( ( ph /\ (/) e. W ) -> ( <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` (/) ) -> 1o = (/) ) )
124 123 expimpd 
 |-  ( ph -> ( ( (/) e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` (/) ) ) -> 1o = (/) ) )
125 hasheq0 
 |-  ( x e. _V -> ( ( # ` x ) = 0 <-> x = (/) ) )
126 125 elv 
 |-  ( ( # ` x ) = 0 <-> x = (/) )
127 eleq1 
 |-  ( x = (/) -> ( x e. W <-> (/) e. W ) )
128 fveq2 
 |-  ( x = (/) -> ( T ` x ) = ( T ` (/) ) )
129 128 rneqd 
 |-  ( x = (/) -> ran ( T ` x ) = ran ( T ` (/) ) )
130 129 eleq2d 
 |-  ( x = (/) -> ( <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) <-> <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` (/) ) ) )
131 127 130 anbi12d 
 |-  ( x = (/) -> ( ( x e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) <-> ( (/) e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` (/) ) ) ) )
132 126 131 sylbi 
 |-  ( ( # ` x ) = 0 -> ( ( x e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) <-> ( (/) e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` (/) ) ) ) )
133 132 eqcoms 
 |-  ( 0 = ( # ` x ) -> ( ( x e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) <-> ( (/) e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` (/) ) ) ) )
134 133 imbi1d 
 |-  ( 0 = ( # ` x ) -> ( ( ( x e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) -> 1o = (/) ) <-> ( ( (/) e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` (/) ) ) -> 1o = (/) ) ) )
135 124 134 syl5ibrcom 
 |-  ( ph -> ( 0 = ( # ` x ) -> ( ( x e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) -> 1o = (/) ) ) )
136 135 com23 
 |-  ( ph -> ( ( x e. W /\ <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) -> ( 0 = ( # ` x ) -> 1o = (/) ) ) )
137 136 expdimp 
 |-  ( ( ph /\ x e. W ) -> ( <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) -> ( 0 = ( # ` x ) -> 1o = (/) ) ) )
138 49 137 mpdd 
 |-  ( ( ph /\ x e. W ) -> ( <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) -> 1o = (/) ) )
139 138 necon3ad 
 |-  ( ( ph /\ x e. W ) -> ( 1o =/= (/) -> -. <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) ) )
140 29 139 mpi 
 |-  ( ( ph /\ x e. W ) -> -. <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) )
141 140 nrexdv 
 |-  ( ph -> -. E. x e. W <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) )
142 eliun 
 |-  ( <" <. A , (/) >. <. B , (/) >. "> e. U_ x e. W ran ( T ` x ) <-> E. x e. W <" <. A , (/) >. <. B , (/) >. "> e. ran ( T ` x ) )
143 141 142 sylnibr 
 |-  ( ph -> -. <" <. A , (/) >. <. B , (/) >. "> e. U_ x e. W ran ( T ` x ) )
144 28 143 eldifd 
 |-  ( ph -> <" <. A , (/) >. <. B , (/) >. "> e. ( W \ U_ x e. W ran ( T ` x ) ) )
145 144 7 eleqtrrdi 
 |-  ( ph -> <" <. A , (/) >. <. B , (/) >. "> e. D )
146 df-s2 
 |-  <" <. A , (/) >. <. B , (/) >. "> = ( <" <. A , (/) >. "> ++ <" <. B , (/) >. "> )
147 2 3 efger 
 |-  .~ Er W
148 147 a1i 
 |-  ( ph -> .~ Er W )
149 148 28 erref 
 |-  ( ph -> <" <. A , (/) >. <. B , (/) >. "> .~ <" <. A , (/) >. <. B , (/) >. "> )
150 146 149 eqbrtrrid 
 |-  ( ph -> ( <" <. A , (/) >. "> ++ <" <. B , (/) >. "> ) .~ <" <. A , (/) >. <. B , (/) >. "> )
151 146 ovexi 
 |-  <" <. A , (/) >. <. B , (/) >. "> e. _V
152 ovex 
 |-  ( <" <. A , (/) >. "> ++ <" <. B , (/) >. "> ) e. _V
153 151 152 elec 
 |-  ( <" <. A , (/) >. <. B , (/) >. "> e. [ ( <" <. A , (/) >. "> ++ <" <. B , (/) >. "> ) ] .~ <-> ( <" <. A , (/) >. "> ++ <" <. B , (/) >. "> ) .~ <" <. A , (/) >. <. B , (/) >. "> )
154 150 153 sylibr 
 |-  ( ph -> <" <. A , (/) >. <. B , (/) >. "> e. [ ( <" <. A , (/) >. "> ++ <" <. B , (/) >. "> ) ] .~ )
155 3 8 vrgpval 
 |-  ( ( I e. V /\ A e. I ) -> ( U ` A ) = [ <" <. A , (/) >. "> ] .~ )
156 9 10 155 syl2anc 
 |-  ( ph -> ( U ` A ) = [ <" <. A , (/) >. "> ] .~ )
157 3 8 vrgpval 
 |-  ( ( I e. V /\ B e. I ) -> ( U ` B ) = [ <" <. B , (/) >. "> ] .~ )
158 9 11 157 syl2anc 
 |-  ( ph -> ( U ` B ) = [ <" <. B , (/) >. "> ] .~ )
159 156 158 oveq12d 
 |-  ( ph -> ( ( U ` A ) .+ ( U ` B ) ) = ( [ <" <. A , (/) >. "> ] .~ .+ [ <" <. B , (/) >. "> ] .~ ) )
160 17 s1cld 
 |-  ( ph -> <" <. A , (/) >. "> e. Word ( I X. 2o ) )
161 160 27 eleqtrrd 
 |-  ( ph -> <" <. A , (/) >. "> e. W )
162 19 s1cld 
 |-  ( ph -> <" <. B , (/) >. "> e. Word ( I X. 2o ) )
163 162 27 eleqtrrd 
 |-  ( ph -> <" <. B , (/) >. "> e. W )
164 2 1 3 4 frgpadd 
 |-  ( ( <" <. A , (/) >. "> e. W /\ <" <. B , (/) >. "> e. W ) -> ( [ <" <. A , (/) >. "> ] .~ .+ [ <" <. B , (/) >. "> ] .~ ) = [ ( <" <. A , (/) >. "> ++ <" <. B , (/) >. "> ) ] .~ )
165 161 163 164 syl2anc 
 |-  ( ph -> ( [ <" <. A , (/) >. "> ] .~ .+ [ <" <. B , (/) >. "> ] .~ ) = [ ( <" <. A , (/) >. "> ++ <" <. B , (/) >. "> ) ] .~ )
166 159 165 eqtrd 
 |-  ( ph -> ( ( U ` A ) .+ ( U ` B ) ) = [ ( <" <. A , (/) >. "> ++ <" <. B , (/) >. "> ) ] .~ )
167 154 166 eleqtrrd 
 |-  ( ph -> <" <. A , (/) >. <. B , (/) >. "> e. ( ( U ` A ) .+ ( U ` B ) ) )
168 145 167 elind 
 |-  ( ph -> <" <. A , (/) >. <. B , (/) >. "> e. ( D i^i ( ( U ` A ) .+ ( U ` B ) ) ) )