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

Metamath Proof Explorer

Theorem ablfacrp

Description: A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups K , L that have trivial intersection and whose product is the whole group. Lemma 6.1C.2 of Shapiro, p. 199. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses ablfacrp.b 
|- B = ( Base ` G )
ablfacrp.o 
|- O = ( od ` G )
ablfacrp.k 
|- K = { x e. B | ( O ` x ) || M }
ablfacrp.l 
|- L = { x e. B | ( O ` x ) || N }
ablfacrp.g 
|- ( ph -> G e. Abel )
ablfacrp.m 
|- ( ph -> M e. NN )
ablfacrp.n 
|- ( ph -> N e. NN )
ablfacrp.1 
|- ( ph -> ( M gcd N ) = 1 )
ablfacrp.2 
|- ( ph -> ( # ` B ) = ( M x. N ) )
ablfacrp.z 
|- .0. = ( 0g ` G )
ablfacrp.s 
|- .(+) = ( LSSum ` G )
Assertion ablfacrp 
|- ( ph -> ( ( K i^i L ) = { .0. } /\ ( K .(+) L ) = B ) )

Proof

Step Hyp Ref Expression
1 ablfacrp.b 
 |-  B = ( Base ` G )
2 ablfacrp.o 
 |-  O = ( od ` G )
3 ablfacrp.k 
 |-  K = { x e. B | ( O ` x ) || M }
4 ablfacrp.l 
 |-  L = { x e. B | ( O ` x ) || N }
5 ablfacrp.g 
 |-  ( ph -> G e. Abel )
6 ablfacrp.m 
 |-  ( ph -> M e. NN )
7 ablfacrp.n 
 |-  ( ph -> N e. NN )
8 ablfacrp.1 
 |-  ( ph -> ( M gcd N ) = 1 )
9 ablfacrp.2 
 |-  ( ph -> ( # ` B ) = ( M x. N ) )
10 ablfacrp.z 
 |-  .0. = ( 0g ` G )
11 ablfacrp.s 
 |-  .(+) = ( LSSum ` G )
12 3 4 ineq12i 
 |-  ( K i^i L ) = ( { x e. B | ( O ` x ) || M } i^i { x e. B | ( O ` x ) || N } )
13 inrab 
 |-  ( { x e. B | ( O ` x ) || M } i^i { x e. B | ( O ` x ) || N } ) = { x e. B | ( ( O ` x ) || M /\ ( O ` x ) || N ) }
14 12 13 eqtri 
 |-  ( K i^i L ) = { x e. B | ( ( O ` x ) || M /\ ( O ` x ) || N ) }
15 1 2 odcl 
 |-  ( x e. B -> ( O ` x ) e. NN0 )
16 15 adantl 
 |-  ( ( ph /\ x e. B ) -> ( O ` x ) e. NN0 )
17 16 nn0zd 
 |-  ( ( ph /\ x e. B ) -> ( O ` x ) e. ZZ )
18 6 nnzd 
 |-  ( ph -> M e. ZZ )
19 18 adantr 
 |-  ( ( ph /\ x e. B ) -> M e. ZZ )
20 7 nnzd 
 |-  ( ph -> N e. ZZ )
21 20 adantr 
 |-  ( ( ph /\ x e. B ) -> N e. ZZ )
22 dvdsgcd 
 |-  ( ( ( O ` x ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( O ` x ) || M /\ ( O ` x ) || N ) -> ( O ` x ) || ( M gcd N ) ) )
23 17 19 21 22 syl3anc 
 |-  ( ( ph /\ x e. B ) -> ( ( ( O ` x ) || M /\ ( O ` x ) || N ) -> ( O ` x ) || ( M gcd N ) ) )
24 23 3impia 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> ( O ` x ) || ( M gcd N ) )
25 8 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> ( M gcd N ) = 1 )
26 24 25 breqtrd 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> ( O ` x ) || 1 )
27 simp2 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> x e. B )
28 dvds1 
 |-  ( ( O ` x ) e. NN0 -> ( ( O ` x ) || 1 <-> ( O ` x ) = 1 ) )
29 27 15 28 3syl 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> ( ( O ` x ) || 1 <-> ( O ` x ) = 1 ) )
30 26 29 mpbid 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> ( O ` x ) = 1 )
31 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
32 5 31 syl 
 |-  ( ph -> G e. Grp )
33 32 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> G e. Grp )
34 2 10 1 odeq1 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( O ` x ) = 1 <-> x = .0. ) )
35 33 27 34 syl2anc 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> ( ( O ` x ) = 1 <-> x = .0. ) )
36 30 35 mpbid 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> x = .0. )
37 velsn 
 |-  ( x e. { .0. } <-> x = .0. )
38 36 37 sylibr 
 |-  ( ( ph /\ x e. B /\ ( ( O ` x ) || M /\ ( O ` x ) || N ) ) -> x e. { .0. } )
39 38 rabssdv 
 |-  ( ph -> { x e. B | ( ( O ` x ) || M /\ ( O ` x ) || N ) } C_ { .0. } )
40 14 39 eqsstrid 
 |-  ( ph -> ( K i^i L ) C_ { .0. } )
41 2 1 oddvdssubg 
 |-  ( ( G e. Abel /\ M e. ZZ ) -> { x e. B | ( O ` x ) || M } e. ( SubGrp ` G ) )
42 5 18 41 syl2anc 
 |-  ( ph -> { x e. B | ( O ` x ) || M } e. ( SubGrp ` G ) )
43 3 42 eqeltrid 
 |-  ( ph -> K e. ( SubGrp ` G ) )
44 10 subg0cl 
 |-  ( K e. ( SubGrp ` G ) -> .0. e. K )
45 43 44 syl 
 |-  ( ph -> .0. e. K )
46 2 1 oddvdssubg 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> { x e. B | ( O ` x ) || N } e. ( SubGrp ` G ) )
47 5 20 46 syl2anc 
 |-  ( ph -> { x e. B | ( O ` x ) || N } e. ( SubGrp ` G ) )
48 4 47 eqeltrid 
 |-  ( ph -> L e. ( SubGrp ` G ) )
49 10 subg0cl 
 |-  ( L e. ( SubGrp ` G ) -> .0. e. L )
50 48 49 syl 
 |-  ( ph -> .0. e. L )
51 45 50 elind 
 |-  ( ph -> .0. e. ( K i^i L ) )
52 51 snssd 
 |-  ( ph -> { .0. } C_ ( K i^i L ) )
53 40 52 eqssd 
 |-  ( ph -> ( K i^i L ) = { .0. } )
54 11 lsmsubg2 
 |-  ( ( G e. Abel /\ K e. ( SubGrp ` G ) /\ L e. ( SubGrp ` G ) ) -> ( K .(+) L ) e. ( SubGrp ` G ) )
55 5 43 48 54 syl3anc 
 |-  ( ph -> ( K .(+) L ) e. ( SubGrp ` G ) )
56 1 subgss 
 |-  ( ( K .(+) L ) e. ( SubGrp ` G ) -> ( K .(+) L ) C_ B )
57 55 56 syl 
 |-  ( ph -> ( K .(+) L ) C_ B )
58 eqid 
 |-  ( .g ` G ) = ( .g ` G )
59 1 58 mulg1 
 |-  ( g e. B -> ( 1 ( .g ` G ) g ) = g )
60 59 adantl 
 |-  ( ( ph /\ g e. B ) -> ( 1 ( .g ` G ) g ) = g )
61 bezout 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> E. a e. ZZ E. b e. ZZ ( M gcd N ) = ( ( M x. a ) + ( N x. b ) ) )
62 18 20 61 syl2anc 
 |-  ( ph -> E. a e. ZZ E. b e. ZZ ( M gcd N ) = ( ( M x. a ) + ( N x. b ) ) )
63 62 adantr 
 |-  ( ( ph /\ g e. B ) -> E. a e. ZZ E. b e. ZZ ( M gcd N ) = ( ( M x. a ) + ( N x. b ) ) )
64 8 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( M gcd N ) = 1 )
65 64 eqeq1d 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( M gcd N ) = ( ( M x. a ) + ( N x. b ) ) <-> 1 = ( ( M x. a ) + ( N x. b ) ) ) )
66 18 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> M e. ZZ )
67 simprl 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
68 66 67 zmulcld 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( M x. a ) e. ZZ )
69 68 zcnd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( M x. a ) e. CC )
70 20 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> N e. ZZ )
71 simprr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ )
72 70 71 zmulcld 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( N x. b ) e. ZZ )
73 72 zcnd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( N x. b ) e. CC )
74 69 73 addcomd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( M x. a ) + ( N x. b ) ) = ( ( N x. b ) + ( M x. a ) ) )
75 74 oveq1d 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( M x. a ) + ( N x. b ) ) ( .g ` G ) g ) = ( ( ( N x. b ) + ( M x. a ) ) ( .g ` G ) g ) )
76 32 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> G e. Grp )
77 simplr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> g e. B )
78 eqid 
 |-  ( +g ` G ) = ( +g ` G )
79 1 58 78 mulgdir 
 |-  ( ( G e. Grp /\ ( ( N x. b ) e. ZZ /\ ( M x. a ) e. ZZ /\ g e. B ) ) -> ( ( ( N x. b ) + ( M x. a ) ) ( .g ` G ) g ) = ( ( ( N x. b ) ( .g ` G ) g ) ( +g ` G ) ( ( M x. a ) ( .g ` G ) g ) ) )
80 76 72 68 77 79 syl13anc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( N x. b ) + ( M x. a ) ) ( .g ` G ) g ) = ( ( ( N x. b ) ( .g ` G ) g ) ( +g ` G ) ( ( M x. a ) ( .g ` G ) g ) ) )
81 75 80 eqtrd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( M x. a ) + ( N x. b ) ) ( .g ` G ) g ) = ( ( ( N x. b ) ( .g ` G ) g ) ( +g ` G ) ( ( M x. a ) ( .g ` G ) g ) ) )
82 43 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> K e. ( SubGrp ` G ) )
83 48 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> L e. ( SubGrp ` G ) )
84 1 58 mulgcl 
 |-  ( ( G e. Grp /\ ( N x. b ) e. ZZ /\ g e. B ) -> ( ( N x. b ) ( .g ` G ) g ) e. B )
85 76 72 77 84 syl3anc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( N x. b ) ( .g ` G ) g ) e. B )
86 1 2 odcl 
 |-  ( g e. B -> ( O ` g ) e. NN0 )
87 86 ad2antlr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` g ) e. NN0 )
88 87 nn0zd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` g ) e. ZZ )
89 66 70 zmulcld 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( M x. N ) e. ZZ )
90 6 7 nnmulcld 
 |-  ( ph -> ( M x. N ) e. NN )
91 90 nnnn0d 
 |-  ( ph -> ( M x. N ) e. NN0 )
92 9 91 eqeltrd 
 |-  ( ph -> ( # ` B ) e. NN0 )
93 1 fvexi 
 |-  B e. _V
94 hashclb 
 |-  ( B e. _V -> ( B e. Fin <-> ( # ` B ) e. NN0 ) )
95 93 94 ax-mp 
 |-  ( B e. Fin <-> ( # ` B ) e. NN0 )
96 92 95 sylibr 
 |-  ( ph -> B e. Fin )
97 96 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> B e. Fin )
98 1 2 oddvds2 
 |-  ( ( G e. Grp /\ B e. Fin /\ g e. B ) -> ( O ` g ) || ( # ` B ) )
99 76 97 77 98 syl3anc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` g ) || ( # ` B ) )
100 9 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( # ` B ) = ( M x. N ) )
101 99 100 breqtrd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` g ) || ( M x. N ) )
102 88 89 71 101 dvdsmultr1d 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` g ) || ( ( M x. N ) x. b ) )
103 66 zcnd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> M e. CC )
104 70 zcnd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> N e. CC )
105 71 zcnd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
106 103 104 105 mulassd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( M x. N ) x. b ) = ( M x. ( N x. b ) ) )
107 102 106 breqtrd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` g ) || ( M x. ( N x. b ) ) )
108 1 2 58 odmulgid 
 |-  ( ( ( G e. Grp /\ g e. B /\ ( N x. b ) e. ZZ ) /\ M e. ZZ ) -> ( ( O ` ( ( N x. b ) ( .g ` G ) g ) ) || M <-> ( O ` g ) || ( M x. ( N x. b ) ) ) )
109 76 77 72 66 108 syl31anc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( O ` ( ( N x. b ) ( .g ` G ) g ) ) || M <-> ( O ` g ) || ( M x. ( N x. b ) ) ) )
110 107 109 mpbird 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` ( ( N x. b ) ( .g ` G ) g ) ) || M )
111 fveq2 
 |-  ( x = ( ( N x. b ) ( .g ` G ) g ) -> ( O ` x ) = ( O ` ( ( N x. b ) ( .g ` G ) g ) ) )
112 111 breq1d 
 |-  ( x = ( ( N x. b ) ( .g ` G ) g ) -> ( ( O ` x ) || M <-> ( O ` ( ( N x. b ) ( .g ` G ) g ) ) || M ) )
113 112 3 elrab2 
 |-  ( ( ( N x. b ) ( .g ` G ) g ) e. K <-> ( ( ( N x. b ) ( .g ` G ) g ) e. B /\ ( O ` ( ( N x. b ) ( .g ` G ) g ) ) || M ) )
114 85 110 113 sylanbrc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( N x. b ) ( .g ` G ) g ) e. K )
115 1 58 mulgcl 
 |-  ( ( G e. Grp /\ ( M x. a ) e. ZZ /\ g e. B ) -> ( ( M x. a ) ( .g ` G ) g ) e. B )
116 76 68 77 115 syl3anc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( M x. a ) ( .g ` G ) g ) e. B )
117 88 89 67 101 dvdsmultr1d 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` g ) || ( ( M x. N ) x. a ) )
118 zcn 
 |-  ( a e. ZZ -> a e. CC )
119 118 ad2antrl 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
120 mulass 
 |-  ( ( M e. CC /\ N e. CC /\ a e. CC ) -> ( ( M x. N ) x. a ) = ( M x. ( N x. a ) ) )
121 mul12 
 |-  ( ( M e. CC /\ N e. CC /\ a e. CC ) -> ( M x. ( N x. a ) ) = ( N x. ( M x. a ) ) )
122 120 121 eqtrd 
 |-  ( ( M e. CC /\ N e. CC /\ a e. CC ) -> ( ( M x. N ) x. a ) = ( N x. ( M x. a ) ) )
123 103 104 119 122 syl3anc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( M x. N ) x. a ) = ( N x. ( M x. a ) ) )
124 117 123 breqtrd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` g ) || ( N x. ( M x. a ) ) )
125 1 2 58 odmulgid 
 |-  ( ( ( G e. Grp /\ g e. B /\ ( M x. a ) e. ZZ ) /\ N e. ZZ ) -> ( ( O ` ( ( M x. a ) ( .g ` G ) g ) ) || N <-> ( O ` g ) || ( N x. ( M x. a ) ) ) )
126 76 77 68 70 125 syl31anc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( O ` ( ( M x. a ) ( .g ` G ) g ) ) || N <-> ( O ` g ) || ( N x. ( M x. a ) ) ) )
127 124 126 mpbird 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( O ` ( ( M x. a ) ( .g ` G ) g ) ) || N )
128 fveq2 
 |-  ( x = ( ( M x. a ) ( .g ` G ) g ) -> ( O ` x ) = ( O ` ( ( M x. a ) ( .g ` G ) g ) ) )
129 128 breq1d 
 |-  ( x = ( ( M x. a ) ( .g ` G ) g ) -> ( ( O ` x ) || N <-> ( O ` ( ( M x. a ) ( .g ` G ) g ) ) || N ) )
130 129 4 elrab2 
 |-  ( ( ( M x. a ) ( .g ` G ) g ) e. L <-> ( ( ( M x. a ) ( .g ` G ) g ) e. B /\ ( O ` ( ( M x. a ) ( .g ` G ) g ) ) || N ) )
131 116 127 130 sylanbrc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( M x. a ) ( .g ` G ) g ) e. L )
132 78 11 lsmelvali 
 |-  ( ( ( K e. ( SubGrp ` G ) /\ L e. ( SubGrp ` G ) ) /\ ( ( ( N x. b ) ( .g ` G ) g ) e. K /\ ( ( M x. a ) ( .g ` G ) g ) e. L ) ) -> ( ( ( N x. b ) ( .g ` G ) g ) ( +g ` G ) ( ( M x. a ) ( .g ` G ) g ) ) e. ( K .(+) L ) )
133 82 83 114 131 132 syl22anc 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( N x. b ) ( .g ` G ) g ) ( +g ` G ) ( ( M x. a ) ( .g ` G ) g ) ) e. ( K .(+) L ) )
134 81 133 eqeltrd 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( M x. a ) + ( N x. b ) ) ( .g ` G ) g ) e. ( K .(+) L ) )
135 oveq1 
 |-  ( 1 = ( ( M x. a ) + ( N x. b ) ) -> ( 1 ( .g ` G ) g ) = ( ( ( M x. a ) + ( N x. b ) ) ( .g ` G ) g ) )
136 135 eleq1d 
 |-  ( 1 = ( ( M x. a ) + ( N x. b ) ) -> ( ( 1 ( .g ` G ) g ) e. ( K .(+) L ) <-> ( ( ( M x. a ) + ( N x. b ) ) ( .g ` G ) g ) e. ( K .(+) L ) ) )
137 134 136 syl5ibrcom 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( 1 = ( ( M x. a ) + ( N x. b ) ) -> ( 1 ( .g ` G ) g ) e. ( K .(+) L ) ) )
138 65 137 sylbid 
 |-  ( ( ( ph /\ g e. B ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( M gcd N ) = ( ( M x. a ) + ( N x. b ) ) -> ( 1 ( .g ` G ) g ) e. ( K .(+) L ) ) )
139 138 rexlimdvva 
 |-  ( ( ph /\ g e. B ) -> ( E. a e. ZZ E. b e. ZZ ( M gcd N ) = ( ( M x. a ) + ( N x. b ) ) -> ( 1 ( .g ` G ) g ) e. ( K .(+) L ) ) )
140 63 139 mpd 
 |-  ( ( ph /\ g e. B ) -> ( 1 ( .g ` G ) g ) e. ( K .(+) L ) )
141 60 140 eqeltrrd 
 |-  ( ( ph /\ g e. B ) -> g e. ( K .(+) L ) )
142 57 141 eqelssd 
 |-  ( ph -> ( K .(+) L ) = B )
143 53 142 jca 
 |-  ( ph -> ( ( K i^i L ) = { .0. } /\ ( K .(+) L ) = B ) )