Metamath Proof Explorer

Theorem 1arithufdlem3

Description: Lemma for 1arithufd . If a product ( Y .x. X ) can be written as a product of primes, with X non-unit, nonzero, so can X . (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses 1arithufd.b 
|- B = ( Base ` R )
1arithufd.0 
|- .0. = ( 0g ` R )
1arithufd.u 
|- U = ( Unit ` R )
1arithufd.p 
|- P = ( RPrime ` R )
1arithufd.m 
|- M = ( mulGrp ` R )
1arithufd.r 
|- ( ph -> R e. UFD )
1arithufdlem.2 
|- ( ph -> -. R e. DivRing )
1arithufdlem.s 
|- S = { x e. B | E. f e. Word P x = ( M gsum f ) }
1arithufdlem.3 
|- ( ph -> X e. B )
1arithufdlem.4 
|- ( ph -> -. X e. U )
1arithufdlem.5 
|- ( ph -> X =/= .0. )
1arithufdlem3.p 
|- .x. = ( .r ` R )
1arithufdlem3.y 
|- ( ph -> Y e. B )
1arithufdlem3.1 
|- ( ph -> ( Y .x. X ) e. S )
Assertion 1arithufdlem3 
|- ( ph -> X e. S )

Proof

Step Hyp Ref Expression
1 1arithufd.b 
 |-  B = ( Base ` R )
2 1arithufd.0 
 |-  .0. = ( 0g ` R )
3 1arithufd.u 
 |-  U = ( Unit ` R )
4 1arithufd.p 
 |-  P = ( RPrime ` R )
5 1arithufd.m 
 |-  M = ( mulGrp ` R )
6 1arithufd.r 
 |-  ( ph -> R e. UFD )
7 1arithufdlem.2 
 |-  ( ph -> -. R e. DivRing )
8 1arithufdlem.s 
 |-  S = { x e. B | E. f e. Word P x = ( M gsum f ) }
9 1arithufdlem.3 
 |-  ( ph -> X e. B )
10 1arithufdlem.4 
 |-  ( ph -> -. X e. U )
11 1arithufdlem.5 
 |-  ( ph -> X =/= .0. )
12 1arithufdlem3.p 
 |-  .x. = ( .r ` R )
13 1arithufdlem3.y 
 |-  ( ph -> Y e. B )
14 1arithufdlem3.1 
 |-  ( ph -> ( Y .x. X ) e. S )
15 oveq1 
 |-  ( y = Y -> ( y .x. X ) = ( Y .x. X ) )
16 15 eqeq1d 
 |-  ( y = Y -> ( ( y .x. X ) = ( M gsum f ) <-> ( Y .x. X ) = ( M gsum f ) ) )
17 13 ad2antrr 
 |-  ( ( ( ph /\ f e. Word P ) /\ ( Y .x. X ) = ( M gsum f ) ) -> Y e. B )
18 simpr 
 |-  ( ( ( ph /\ f e. Word P ) /\ ( Y .x. X ) = ( M gsum f ) ) -> ( Y .x. X ) = ( M gsum f ) )
19 16 17 18 rspcedvdw 
 |-  ( ( ( ph /\ f e. Word P ) /\ ( Y .x. X ) = ( M gsum f ) ) -> E. y e. B ( y .x. X ) = ( M gsum f ) )
20 oveq2 
 |-  ( z = X -> ( y .x. z ) = ( y .x. X ) )
21 20 eqeq1d 
 |-  ( z = X -> ( ( y .x. z ) = ( M gsum f ) <-> ( y .x. X ) = ( M gsum f ) ) )
22 21 rexbidv 
 |-  ( z = X -> ( E. y e. B ( y .x. z ) = ( M gsum f ) <-> E. y e. B ( y .x. X ) = ( M gsum f ) ) )
23 eleq1 
 |-  ( z = X -> ( z e. S <-> X e. S ) )
24 22 23 imbi12d 
 |-  ( z = X -> ( ( E. y e. B ( y .x. z ) = ( M gsum f ) -> z e. S ) <-> ( E. y e. B ( y .x. X ) = ( M gsum f ) -> X e. S ) ) )
25 oveq2 
 |-  ( c = (/) -> ( M gsum c ) = ( M gsum (/) ) )
26 25 eqeq2d 
 |-  ( c = (/) -> ( ( y .x. z ) = ( M gsum c ) <-> ( y .x. z ) = ( M gsum (/) ) ) )
27 26 rexbidv 
 |-  ( c = (/) -> ( E. y e. B ( y .x. z ) = ( M gsum c ) <-> E. y e. B ( y .x. z ) = ( M gsum (/) ) ) )
28 27 imbi1d 
 |-  ( c = (/) -> ( ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) <-> ( E. y e. B ( y .x. z ) = ( M gsum (/) ) -> z e. S ) ) )
29 28 ralbidv 
 |-  ( c = (/) -> ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) <-> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum (/) ) -> z e. S ) ) )
30 29 imbi2d 
 |-  ( c = (/) -> ( ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) ) <-> ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum (/) ) -> z e. S ) ) ) )
31 oveq2 
 |-  ( c = d -> ( M gsum c ) = ( M gsum d ) )
32 31 eqeq2d 
 |-  ( c = d -> ( ( y .x. z ) = ( M gsum c ) <-> ( y .x. z ) = ( M gsum d ) ) )
33 32 rexbidv 
 |-  ( c = d -> ( E. y e. B ( y .x. z ) = ( M gsum c ) <-> E. y e. B ( y .x. z ) = ( M gsum d ) ) )
34 33 imbi1d 
 |-  ( c = d -> ( ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) <-> ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) )
35 34 ralbidv 
 |-  ( c = d -> ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) <-> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) )
36 35 imbi2d 
 |-  ( c = d -> ( ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) ) <-> ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) ) )
37 oveq2 
 |-  ( c = ( d ++ <" p "> ) -> ( M gsum c ) = ( M gsum ( d ++ <" p "> ) ) )
38 37 eqeq2d 
 |-  ( c = ( d ++ <" p "> ) -> ( ( y .x. z ) = ( M gsum c ) <-> ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) ) )
39 38 rexbidv 
 |-  ( c = ( d ++ <" p "> ) -> ( E. y e. B ( y .x. z ) = ( M gsum c ) <-> E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) ) )
40 39 imbi1d 
 |-  ( c = ( d ++ <" p "> ) -> ( ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) <-> ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) ) )
41 40 ralbidv 
 |-  ( c = ( d ++ <" p "> ) -> ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) <-> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) ) )
42 41 imbi2d 
 |-  ( c = ( d ++ <" p "> ) -> ( ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) ) <-> ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) ) ) )
43 oveq2 
 |-  ( c = f -> ( M gsum c ) = ( M gsum f ) )
44 43 eqeq2d 
 |-  ( c = f -> ( ( y .x. z ) = ( M gsum c ) <-> ( y .x. z ) = ( M gsum f ) ) )
45 44 rexbidv 
 |-  ( c = f -> ( E. y e. B ( y .x. z ) = ( M gsum c ) <-> E. y e. B ( y .x. z ) = ( M gsum f ) ) )
46 45 imbi1d 
 |-  ( c = f -> ( ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) <-> ( E. y e. B ( y .x. z ) = ( M gsum f ) -> z e. S ) ) )
47 46 ralbidv 
 |-  ( c = f -> ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) <-> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum f ) -> z e. S ) ) )
48 47 imbi2d 
 |-  ( c = f -> ( ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum c ) -> z e. S ) ) <-> ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum f ) -> z e. S ) ) ) )
49 6 ufdidom 
 |-  ( ph -> R e. IDomn )
50 49 idomcringd 
 |-  ( ph -> R e. CRing )
51 50 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> R e. CRing )
52 simpllr 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> y e. B )
53 simp-4r 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> z e. ( ( B \ U ) \ { .0. } ) )
54 53 eldifad 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> z e. ( B \ U ) )
55 54 eldifad 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> z e. B )
56 simplr 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> ( y .x. z ) = ( M gsum (/) ) )
57 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
58 5 57 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
59 58 gsum0 
 |-  ( M gsum (/) ) = ( 1r ` R )
60 56 59 eqtrdi 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> ( y .x. z ) = ( 1r ` R ) )
61 51 crngringd 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> R e. Ring )
62 3 57 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. U )
63 61 62 syl 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> ( 1r ` R ) e. U )
64 60 63 eqeltrd 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> ( y .x. z ) e. U )
65 3 12 1 unitmulclb 
 |-  ( ( R e. CRing /\ y e. B /\ z e. B ) -> ( ( y .x. z ) e. U <-> ( y e. U /\ z e. U ) ) )
66 65 simplbda 
 |-  ( ( ( R e. CRing /\ y e. B /\ z e. B ) /\ ( y .x. z ) e. U ) -> z e. U )
67 51 52 55 64 66 syl31anc 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> z e. U )
68 54 eldifbd 
 |-  ( ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) /\ -. z e. S ) -> -. z e. U )
69 67 68 condan 
 |-  ( ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ y e. B ) /\ ( y .x. z ) = ( M gsum (/) ) ) -> z e. S )
70 69 r19.29an 
 |-  ( ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) /\ E. y e. B ( y .x. z ) = ( M gsum (/) ) ) -> z e. S )
71 70 ex 
 |-  ( ( ph /\ z e. ( ( B \ U ) \ { .0. } ) ) -> ( E. y e. B ( y .x. z ) = ( M gsum (/) ) -> z e. S ) )
72 71 ralrimiva 
 |-  ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum (/) ) -> z e. S ) )
73 oveq1 
 |-  ( y = w -> ( y .x. t ) = ( w .x. t ) )
74 73 eqeq1d 
 |-  ( y = w -> ( ( y .x. t ) = ( M gsum ( d ++ <" p "> ) ) <-> ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) )
75 74 cbvrexvw 
 |-  ( E. y e. B ( y .x. t ) = ( M gsum ( d ++ <" p "> ) ) <-> E. w e. B ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) )
76 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
77 1 76 12 dvdsr 
 |-  ( p ( ||r ` R ) w <-> ( p e. B /\ E. k e. B ( k .x. p ) = w ) )
78 oveq1 
 |-  ( v = k -> ( v .x. t ) = ( k .x. t ) )
79 78 eqeq1d 
 |-  ( v = k -> ( ( v .x. t ) = ( M gsum d ) <-> ( k .x. t ) = ( M gsum d ) ) )
80 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> k e. B )
81 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
82 6 adantr 
 |-  ( ( ph /\ p e. P ) -> R e. UFD )
83 simpr 
 |-  ( ( ph /\ p e. P ) -> p e. P )
84 1 4 82 83 rprmcl 
 |-  ( ( ph /\ p e. P ) -> p e. B )
85 84 ex 
 |-  ( ph -> ( p e. P -> p e. B ) )
86 85 ssrdv 
 |-  ( ph -> P C_ B )
87 86 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> P C_ B )
88 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> p e. P )
89 87 88 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> p e. B )
90 89 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> p e. B )
91 6 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> R e. UFD )
92 91 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> R e. UFD )
93 88 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> p e. P )
94 4 81 92 93 rprmnz 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> p =/= ( 0g ` R ) )
95 90 94 eldifsnd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> p e. ( B \ { ( 0g ` R ) } ) )
96 5 1 mgpbas 
 |-  B = ( Base ` M )
97 5 crngmgp 
 |-  ( R e. CRing -> M e. CMnd )
98 50 97 syl 
 |-  ( ph -> M e. CMnd )
99 98 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> M e. CMnd )
100 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> ( 0 ..^ ( # ` d ) ) e. _V )
101 eqidd 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> ( # ` d ) = ( # ` d ) )
102 sswrd 
 |-  ( P C_ B -> Word P C_ Word B )
103 86 102 syl 
 |-  ( ph -> Word P C_ Word B )
104 103 sselda 
 |-  ( ( ph /\ d e. Word P ) -> d e. Word B )
105 104 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> d e. Word B )
106 101 105 wrdfd 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> d : ( 0 ..^ ( # ` d ) ) --> B )
107 50 crngringd 
 |-  ( ph -> R e. Ring )
108 107 62 syl 
 |-  ( ph -> ( 1r ` R ) e. U )
109 108 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> ( 1r ` R ) e. U )
110 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> d e. Word P )
111 109 110 wrdfsupp 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> d finSupp ( 1r ` R ) )
112 96 58 99 100 106 111 gsumcl 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> ( M gsum d ) e. B )
113 112 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( M gsum d ) e. B )
114 107 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> R e. Ring )
115 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> t e. ( ( B \ U ) \ { .0. } ) )
116 115 eldifad 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> t e. ( B \ U ) )
117 116 eldifad 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> t e. B )
118 117 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> t e. B )
119 1 12 114 80 118 ringcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( k .x. t ) e. B )
120 49 idomdomd 
 |-  ( ph -> R e. Domn )
121 120 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> R e. Domn )
122 50 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> R e. CRing )
123 1 12 122 90 113 crngcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( p .x. ( M gsum d ) ) = ( ( M gsum d ) .x. p ) )
124 simpr 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) )
125 5 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
126 107 125 syl 
 |-  ( ph -> M e. Mnd )
127 126 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> M e. Mnd )
128 5 12 mgpplusg 
 |-  .x. = ( +g ` M )
129 96 128 gsumccatsn 
 |-  ( ( M e. Mnd /\ d e. Word B /\ p e. B ) -> ( M gsum ( d ++ <" p "> ) ) = ( ( M gsum d ) .x. p ) )
130 127 105 89 129 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> ( M gsum ( d ++ <" p "> ) ) = ( ( M gsum d ) .x. p ) )
131 124 130 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> ( w .x. t ) = ( ( M gsum d ) .x. p ) )
132 131 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( w .x. t ) = ( ( M gsum d ) .x. p ) )
133 1 12 114 80 90 118 ringassd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( ( k .x. p ) .x. t ) = ( k .x. ( p .x. t ) ) )
134 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( k .x. p ) = w )
135 134 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( ( k .x. p ) .x. t ) = ( w .x. t ) )
136 1 12 122 80 90 118 crng12d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( k .x. ( p .x. t ) ) = ( p .x. ( k .x. t ) ) )
137 133 135 136 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( w .x. t ) = ( p .x. ( k .x. t ) ) )
138 123 132 137 3eqtr2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( p .x. ( M gsum d ) ) = ( p .x. ( k .x. t ) ) )
139 1 81 12 95 113 119 121 138 domnlcan 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( M gsum d ) = ( k .x. t ) )
140 139 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( k .x. t ) = ( M gsum d ) )
141 79 80 140 rspcedvdw 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> E. v e. B ( v .x. t ) = ( M gsum d ) )
142 oveq1 
 |-  ( y = v -> ( y .x. t ) = ( v .x. t ) )
143 142 eqeq1d 
 |-  ( y = v -> ( ( y .x. t ) = ( M gsum d ) <-> ( v .x. t ) = ( M gsum d ) ) )
144 143 cbvrexvw 
 |-  ( E. y e. B ( y .x. t ) = ( M gsum d ) <-> E. v e. B ( v .x. t ) = ( M gsum d ) )
145 141 144 sylibr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> E. y e. B ( y .x. t ) = ( M gsum d ) )
146 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = w ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) -> t e. ( ( B \ U ) \ { .0. } ) )
147 oveq2 
 |-  ( z = t -> ( y .x. z ) = ( y .x. t ) )
148 147 eqeq1d 
 |-  ( z = t -> ( ( y .x. z ) = ( M gsum d ) <-> ( y .x. t ) = ( M gsum d ) ) )
149 148 rexbidv 
 |-  ( z = t -> ( E. y e. B ( y .x. z ) = ( M gsum d ) <-> E. y e. B ( y .x. t ) = ( M gsum d ) ) )
150 eleq1w 
 |-  ( z = t -> ( z e. S <-> t e. S ) )
151 149 150 imbi12d 
 |-  ( z = t -> ( ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) <-> ( E. y e. B ( y .x. t ) = ( M gsum d ) -> t e. S ) ) )
152 151 adantl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = w ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ z = t ) -> ( ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) <-> ( E. y e. B ( y .x. t ) = ( M gsum d ) -> t e. S ) ) )
153 146 152 rspcdv 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = w ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) -> ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) -> ( E. y e. B ( y .x. t ) = ( M gsum d ) -> t e. S ) ) )
154 153 imp 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = w ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) -> ( E. y e. B ( y .x. t ) = ( M gsum d ) -> t e. S ) )
155 154 an72ds 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> ( E. y e. B ( y .x. t ) = ( M gsum d ) -> t e. S ) )
156 145 155 mpd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = w ) -> t e. S )
157 156 r19.29an 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ E. k e. B ( k .x. p ) = w ) -> t e. S )
158 157 adantrl 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ ( p e. B /\ E. k e. B ( k .x. p ) = w ) ) -> t e. S )
159 77 158 sylan2b 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ p ( ||r ` R ) w ) -> t e. S )
160 1 76 12 dvdsr 
 |-  ( p ( ||r ` R ) t <-> ( p e. B /\ E. k e. B ( k .x. p ) = t ) )
161 eqeq1 
 |-  ( x = t -> ( x = ( M gsum f ) <-> t = ( M gsum f ) ) )
162 161 rexbidv 
 |-  ( x = t -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P t = ( M gsum f ) ) )
163 117 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> t e. B )
164 oveq2 
 |-  ( f = <" t "> -> ( M gsum f ) = ( M gsum <" t "> ) )
165 164 eqeq2d 
 |-  ( f = <" t "> -> ( t = ( M gsum f ) <-> t = ( M gsum <" t "> ) ) )
166 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> ( k .x. p ) = t )
167 49 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> R e. IDomn )
168 167 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> R e. IDomn )
169 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> k e. U )
170 88 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> p e. P )
171 170 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> p e. P )
172 4 3 12 168 169 171 unitmulrprm 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> ( k .x. p ) e. P )
173 166 172 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> t e. P )
174 173 s1cld 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> <" t "> e. Word P )
175 96 gsumws1 
 |-  ( t e. B -> ( M gsum <" t "> ) = t )
176 163 175 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> ( M gsum <" t "> ) = t )
177 176 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> t = ( M gsum <" t "> ) )
178 165 174 177 rspcedvdw 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> E. f e. Word P t = ( M gsum f ) )
179 162 163 178 elrabd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> t e. { x e. B | E. f e. Word P x = ( M gsum f ) } )
180 179 8 eleqtrrdi 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ k e. U ) -> t e. S )
181 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ -. k e. U ) -> ( k .x. p ) = t )
182 91 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> R e. UFD )
183 182 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ -. k e. U ) -> R e. UFD )
184 7 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> -. R e. DivRing )
185 184 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ -. k e. U ) -> -. R e. DivRing )
186 oveq1 
 |-  ( v = w -> ( v .x. k ) = ( w .x. k ) )
187 186 eqeq1d 
 |-  ( v = w -> ( ( v .x. k ) = ( M gsum d ) <-> ( w .x. k ) = ( M gsum d ) ) )
188 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> w e. B )
189 107 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> R e. Ring )
190 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> k e. B )
191 1 12 189 188 190 ringcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> ( w .x. k ) e. B )
192 112 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> ( M gsum d ) e. B )
193 89 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> p e. B )
194 4 2 182 170 rprmnz 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> p =/= .0. )
195 193 194 eldifsnd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> p e. ( B \ { .0. } ) )
196 1 12 189 188 190 193 ringassd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> ( ( w .x. k ) .x. p ) = ( w .x. ( k .x. p ) ) )
197 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> ( k .x. p ) = t )
198 197 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> ( w .x. ( k .x. p ) ) = ( w .x. t ) )
199 131 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> ( w .x. t ) = ( ( M gsum d ) .x. p ) )
200 196 198 199 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> ( ( w .x. k ) .x. p ) = ( ( M gsum d ) .x. p ) )
201 1 2 12 191 192 195 167 200 idomrcan 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> ( w .x. k ) = ( M gsum d ) )
202 187 188 201 rspcedvdw 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> E. v e. B ( v .x. k ) = ( M gsum d ) )
203 oveq1 
 |-  ( y = v -> ( y .x. k ) = ( v .x. k ) )
204 203 eqeq1d 
 |-  ( y = v -> ( ( y .x. k ) = ( M gsum d ) <-> ( v .x. k ) = ( M gsum d ) ) )
205 204 cbvrexvw 
 |-  ( E. y e. B ( y .x. k ) = ( M gsum d ) <-> E. v e. B ( v .x. k ) = ( M gsum d ) )
206 202 205 sylibr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> E. y e. B ( y .x. k ) = ( M gsum d ) )
207 206 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ -. k e. U ) -> E. y e. B ( y .x. k ) = ( M gsum d ) )
208 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ -. k e. U ) -> k e. B )
209 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ -. k e. U ) -> -. k e. U )
210 208 209 eldifd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ -. k e. U ) -> k e. ( B \ U ) )
211 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> k = .0. )
212 211 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> ( k .x. p ) = ( .0. .x. p ) )
213 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> ( k .x. p ) = t )
214 107 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> R e. Ring )
215 84 adantlr 
 |-  ( ( ( ph /\ d e. Word P ) /\ p e. P ) -> p e. B )
216 215 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> p e. B )
217 1 12 2 214 216 ringlzd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> ( .0. .x. p ) = .0. )
218 212 213 217 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> t = .0. )
219 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> t e. ( ( B \ U ) \ { .0. } ) )
220 eldifsni 
 |-  ( t e. ( ( B \ U ) \ { .0. } ) -> t =/= .0. )
221 219 220 syl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> t =/= .0. )
222 221 neneqd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ k = .0. ) -> -. t = .0. )
223 218 222 pm2.65da 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) -> -. k = .0. )
224 223 neqned 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) -> k =/= .0. )
225 224 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ -. k e. U ) -> k =/= .0. )
226 210 225 eldifsnd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ ( k .x. p ) = t ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ -. k e. U ) -> k e. ( ( B \ U ) \ { .0. } ) )
227 226 an72ds 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ -. k e. U ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> k e. ( ( B \ U ) \ { .0. } ) )
228 oveq2 
 |-  ( z = k -> ( y .x. z ) = ( y .x. k ) )
229 228 eqeq1d 
 |-  ( z = k -> ( ( y .x. z ) = ( M gsum d ) <-> ( y .x. k ) = ( M gsum d ) ) )
230 229 rexbidv 
 |-  ( z = k -> ( E. y e. B ( y .x. z ) = ( M gsum d ) <-> E. y e. B ( y .x. k ) = ( M gsum d ) ) )
231 eleq1w 
 |-  ( z = k -> ( z e. S <-> k e. S ) )
232 230 231 imbi12d 
 |-  ( z = k -> ( ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) <-> ( E. y e. B ( y .x. k ) = ( M gsum d ) -> k e. S ) ) )
233 232 adantl 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ -. k e. U ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ z = k ) -> ( ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) <-> ( E. y e. B ( y .x. k ) = ( M gsum d ) -> k e. S ) ) )
234 227 233 rspcdv 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ -. k e. U ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) -> ( E. y e. B ( y .x. k ) = ( M gsum d ) -> k e. S ) ) )
235 234 imp 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ -. k e. U ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) -> ( E. y e. B ( y .x. k ) = ( M gsum d ) -> k e. S ) )
236 235 an82ds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ -. k e. U ) -> ( E. y e. B ( y .x. k ) = ( M gsum d ) -> k e. S ) )
237 207 236 mpd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ -. k e. U ) -> k e. S )
238 eqeq1 
 |-  ( x = p -> ( x = ( M gsum f ) <-> p = ( M gsum f ) ) )
239 238 rexbidv 
 |-  ( x = p -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P p = ( M gsum f ) ) )
240 oveq2 
 |-  ( f = <" p "> -> ( M gsum f ) = ( M gsum <" p "> ) )
241 240 eqeq2d 
 |-  ( f = <" p "> -> ( p = ( M gsum f ) <-> p = ( M gsum <" p "> ) ) )
242 simpr 
 |-  ( ( ( ph /\ d e. Word P ) /\ p e. P ) -> p e. P )
243 242 s1cld 
 |-  ( ( ( ph /\ d e. Word P ) /\ p e. P ) -> <" p "> e. Word P )
244 96 gsumws1 
 |-  ( p e. B -> ( M gsum <" p "> ) = p )
245 215 244 syl 
 |-  ( ( ( ph /\ d e. Word P ) /\ p e. P ) -> ( M gsum <" p "> ) = p )
246 245 eqcomd 
 |-  ( ( ( ph /\ d e. Word P ) /\ p e. P ) -> p = ( M gsum <" p "> ) )
247 241 243 246 rspcedvdw 
 |-  ( ( ( ph /\ d e. Word P ) /\ p e. P ) -> E. f e. Word P p = ( M gsum f ) )
248 239 215 247 elrabd 
 |-  ( ( ( ph /\ d e. Word P ) /\ p e. P ) -> p e. { x e. B | E. f e. Word P x = ( M gsum f ) } )
249 248 8 eleqtrrdi 
 |-  ( ( ( ph /\ d e. Word P ) /\ p e. P ) -> p e. S )
250 249 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ -. k e. U ) -> p e. S )
251 1 2 3 4 5 183 185 8 12 237 250 1arithufdlem2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ -. k e. U ) -> ( k .x. p ) e. S )
252 181 251 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) /\ -. k e. U ) -> t e. S )
253 180 252 pm2.61dan 
 |-  ( ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ k e. B ) /\ ( k .x. p ) = t ) -> t e. S )
254 253 r19.29an 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ E. k e. B ( k .x. p ) = t ) -> t e. S )
255 254 adantrl 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ ( p e. B /\ E. k e. B ( k .x. p ) = t ) ) -> t e. S )
256 160 255 sylan2b 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) /\ p ( ||r ` R ) t ) -> t e. S )
257 simplr 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> w e. B )
258 1 76 12 dvdsrmul 
 |-  ( ( p e. B /\ ( M gsum d ) e. B ) -> p ( ||r ` R ) ( ( M gsum d ) .x. p ) )
259 89 112 258 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> p ( ||r ` R ) ( ( M gsum d ) .x. p ) )
260 259 131 breqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> p ( ||r ` R ) ( w .x. t ) )
261 1 4 76 12 91 88 257 117 260 rprmdvds 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> ( p ( ||r ` R ) w \/ p ( ||r ` R ) t ) )
262 159 256 261 mpjaodan 
 |-  ( ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ w e. B ) /\ ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> t e. S )
263 262 r19.29an 
 |-  ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ E. w e. B ( w .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> t e. S )
264 75 263 sylan2b 
 |-  ( ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) /\ E. y e. B ( y .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) -> t e. S )
265 264 ex 
 |-  ( ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) /\ t e. ( ( B \ U ) \ { .0. } ) ) -> ( E. y e. B ( y .x. t ) = ( M gsum ( d ++ <" p "> ) ) -> t e. S ) )
266 265 ralrimiva 
 |-  ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) -> A. t e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. t ) = ( M gsum ( d ++ <" p "> ) ) -> t e. S ) )
267 147 eqeq1d 
 |-  ( z = t -> ( ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) <-> ( y .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) )
268 267 rexbidv 
 |-  ( z = t -> ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) <-> E. y e. B ( y .x. t ) = ( M gsum ( d ++ <" p "> ) ) ) )
269 268 150 imbi12d 
 |-  ( z = t -> ( ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) <-> ( E. y e. B ( y .x. t ) = ( M gsum ( d ++ <" p "> ) ) -> t e. S ) ) )
270 269 cbvralvw 
 |-  ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) <-> A. t e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. t ) = ( M gsum ( d ++ <" p "> ) ) -> t e. S ) )
271 266 270 sylibr 
 |-  ( ( ( ( ph /\ d e. Word P ) /\ p e. P ) /\ A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) )
272 271 ex 
 |-  ( ( ( ph /\ d e. Word P ) /\ p e. P ) -> ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) ) )
273 272 anasss 
 |-  ( ( ph /\ ( d e. Word P /\ p e. P ) ) -> ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) ) )
274 273 expcom 
 |-  ( ( d e. Word P /\ p e. P ) -> ( ph -> ( A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) ) ) )
275 274 a2d 
 |-  ( ( d e. Word P /\ p e. P ) -> ( ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum d ) -> z e. S ) ) -> ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum ( d ++ <" p "> ) ) -> z e. S ) ) ) )
276 30 36 42 48 72 275 wrdind 
 |-  ( f e. Word P -> ( ph -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum f ) -> z e. S ) ) )
277 276 impcom 
 |-  ( ( ph /\ f e. Word P ) -> A. z e. ( ( B \ U ) \ { .0. } ) ( E. y e. B ( y .x. z ) = ( M gsum f ) -> z e. S ) )
278 9 10 eldifd 
 |-  ( ph -> X e. ( B \ U ) )
279 278 11 eldifsnd 
 |-  ( ph -> X e. ( ( B \ U ) \ { .0. } ) )
280 279 adantr 
 |-  ( ( ph /\ f e. Word P ) -> X e. ( ( B \ U ) \ { .0. } ) )
281 24 277 280 rspcdva 
 |-  ( ( ph /\ f e. Word P ) -> ( E. y e. B ( y .x. X ) = ( M gsum f ) -> X e. S ) )
282 281 imp 
 |-  ( ( ( ph /\ f e. Word P ) /\ E. y e. B ( y .x. X ) = ( M gsum f ) ) -> X e. S )
283 19 282 syldan 
 |-  ( ( ( ph /\ f e. Word P ) /\ ( Y .x. X ) = ( M gsum f ) ) -> X e. S )
284 14 8 eleqtrdi 
 |-  ( ph -> ( Y .x. X ) e. { x e. B | E. f e. Word P x = ( M gsum f ) } )
285 eqeq1 
 |-  ( x = ( Y .x. X ) -> ( x = ( M gsum f ) <-> ( Y .x. X ) = ( M gsum f ) ) )
286 285 rexbidv 
 |-  ( x = ( Y .x. X ) -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P ( Y .x. X ) = ( M gsum f ) ) )
287 286 elrab 
 |-  ( ( Y .x. X ) e. { x e. B | E. f e. Word P x = ( M gsum f ) } <-> ( ( Y .x. X ) e. B /\ E. f e. Word P ( Y .x. X ) = ( M gsum f ) ) )
288 284 287 sylib 
 |-  ( ph -> ( ( Y .x. X ) e. B /\ E. f e. Word P ( Y .x. X ) = ( M gsum f ) ) )
289 288 simprd 
 |-  ( ph -> E. f e. Word P ( Y .x. X ) = ( M gsum f ) )
290 283 289 r19.29a 
 |-  ( ph -> X e. S )