Metamath Proof Explorer

Theorem evl1gprodd

Description: Polynomial evaluation builder for a finite group product of polynomials. (Contributed by metakunt, 29-Apr-2025)

Ref Expression
Hypotheses evl1gprodd.1 
|- O = ( eval1 ` R )
evl1gprodd.2 
|- P = ( Poly1 ` R )
evl1gprodd.3 
|- Q = ( mulGrp ` P )
evl1gprodd.4 
|- B = ( Base ` R )
evl1gprodd.5 
|- U = ( Base ` P )
evl1gprodd.6 
|- S = ( mulGrp ` R )
evl1gprodd.7 
|- ( ph -> R e. CRing )
evl1gprodd.8 
|- ( ph -> Y e. B )
evl1gprodd.9 
|- ( ph -> A. x e. N M e. U )
evl1gprodd.10 
|- ( ph -> N e. Fin )
Assertion evl1gprodd 
|- ( ph -> ( ( O ` ( Q gsum ( x e. N |-> M ) ) ) ` Y ) = ( S gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 evl1gprodd.1 
 |-  O = ( eval1 ` R )
2 evl1gprodd.2 
 |-  P = ( Poly1 ` R )
3 evl1gprodd.3 
 |-  Q = ( mulGrp ` P )
4 evl1gprodd.4 
 |-  B = ( Base ` R )
5 evl1gprodd.5 
 |-  U = ( Base ` P )
6 evl1gprodd.6 
 |-  S = ( mulGrp ` R )
7 evl1gprodd.7 
 |-  ( ph -> R e. CRing )
8 evl1gprodd.8 
 |-  ( ph -> Y e. B )
9 evl1gprodd.9 
 |-  ( ph -> A. x e. N M e. U )
10 evl1gprodd.10 
 |-  ( ph -> N e. Fin )
11 mpteq1 
 |-  ( a = (/) -> ( x e. a |-> M ) = ( x e. (/) |-> M ) )
12 11 oveq2d 
 |-  ( a = (/) -> ( Q gsum ( x e. a |-> M ) ) = ( Q gsum ( x e. (/) |-> M ) ) )
13 12 fveq2d 
 |-  ( a = (/) -> ( O ` ( Q gsum ( x e. a |-> M ) ) ) = ( O ` ( Q gsum ( x e. (/) |-> M ) ) ) )
14 13 fveq1d 
 |-  ( a = (/) -> ( ( O ` ( Q gsum ( x e. a |-> M ) ) ) ` Y ) = ( ( O ` ( Q gsum ( x e. (/) |-> M ) ) ) ` Y ) )
15 mpteq1 
 |-  ( a = (/) -> ( x e. a |-> ( ( O ` M ) ` Y ) ) = ( x e. (/) |-> ( ( O ` M ) ` Y ) ) )
16 15 oveq2d 
 |-  ( a = (/) -> ( S gsum ( x e. a |-> ( ( O ` M ) ` Y ) ) ) = ( S gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) )
17 14 16 eqeq12d 
 |-  ( a = (/) -> ( ( ( O ` ( Q gsum ( x e. a |-> M ) ) ) ` Y ) = ( S gsum ( x e. a |-> ( ( O ` M ) ` Y ) ) ) <-> ( ( O ` ( Q gsum ( x e. (/) |-> M ) ) ) ` Y ) = ( S gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) ) )
18 mpteq1 
 |-  ( a = b -> ( x e. a |-> M ) = ( x e. b |-> M ) )
19 18 oveq2d 
 |-  ( a = b -> ( Q gsum ( x e. a |-> M ) ) = ( Q gsum ( x e. b |-> M ) ) )
20 19 fveq2d 
 |-  ( a = b -> ( O ` ( Q gsum ( x e. a |-> M ) ) ) = ( O ` ( Q gsum ( x e. b |-> M ) ) ) )
21 20 fveq1d 
 |-  ( a = b -> ( ( O ` ( Q gsum ( x e. a |-> M ) ) ) ` Y ) = ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) )
22 mpteq1 
 |-  ( a = b -> ( x e. a |-> ( ( O ` M ) ` Y ) ) = ( x e. b |-> ( ( O ` M ) ` Y ) ) )
23 22 oveq2d 
 |-  ( a = b -> ( S gsum ( x e. a |-> ( ( O ` M ) ` Y ) ) ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) )
24 21 23 eqeq12d 
 |-  ( a = b -> ( ( ( O ` ( Q gsum ( x e. a |-> M ) ) ) ` Y ) = ( S gsum ( x e. a |-> ( ( O ` M ) ` Y ) ) ) <-> ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) )
25 mpteq1 
 |-  ( a = ( b u. { c } ) -> ( x e. a |-> M ) = ( x e. ( b u. { c } ) |-> M ) )
26 25 oveq2d 
 |-  ( a = ( b u. { c } ) -> ( Q gsum ( x e. a |-> M ) ) = ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) )
27 26 fveq2d 
 |-  ( a = ( b u. { c } ) -> ( O ` ( Q gsum ( x e. a |-> M ) ) ) = ( O ` ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) ) )
28 27 fveq1d 
 |-  ( a = ( b u. { c } ) -> ( ( O ` ( Q gsum ( x e. a |-> M ) ) ) ` Y ) = ( ( O ` ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) ) ` Y ) )
29 mpteq1 
 |-  ( a = ( b u. { c } ) -> ( x e. a |-> ( ( O ` M ) ` Y ) ) = ( x e. ( b u. { c } ) |-> ( ( O ` M ) ` Y ) ) )
30 29 oveq2d 
 |-  ( a = ( b u. { c } ) -> ( S gsum ( x e. a |-> ( ( O ` M ) ` Y ) ) ) = ( S gsum ( x e. ( b u. { c } ) |-> ( ( O ` M ) ` Y ) ) ) )
31 28 30 eqeq12d 
 |-  ( a = ( b u. { c } ) -> ( ( ( O ` ( Q gsum ( x e. a |-> M ) ) ) ` Y ) = ( S gsum ( x e. a |-> ( ( O ` M ) ` Y ) ) ) <-> ( ( O ` ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) ) ` Y ) = ( S gsum ( x e. ( b u. { c } ) |-> ( ( O ` M ) ` Y ) ) ) ) )
32 mpteq1 
 |-  ( a = N -> ( x e. a |-> M ) = ( x e. N |-> M ) )
33 32 oveq2d 
 |-  ( a = N -> ( Q gsum ( x e. a |-> M ) ) = ( Q gsum ( x e. N |-> M ) ) )
34 33 fveq2d 
 |-  ( a = N -> ( O ` ( Q gsum ( x e. a |-> M ) ) ) = ( O ` ( Q gsum ( x e. N |-> M ) ) ) )
35 34 fveq1d 
 |-  ( a = N -> ( ( O ` ( Q gsum ( x e. a |-> M ) ) ) ` Y ) = ( ( O ` ( Q gsum ( x e. N |-> M ) ) ) ` Y ) )
36 mpteq1 
 |-  ( a = N -> ( x e. a |-> ( ( O ` M ) ` Y ) ) = ( x e. N |-> ( ( O ` M ) ` Y ) ) )
37 36 oveq2d 
 |-  ( a = N -> ( S gsum ( x e. a |-> ( ( O ` M ) ` Y ) ) ) = ( S gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) )
38 35 37 eqeq12d 
 |-  ( a = N -> ( ( ( O ` ( Q gsum ( x e. a |-> M ) ) ) ` Y ) = ( S gsum ( x e. a |-> ( ( O ` M ) ` Y ) ) ) <-> ( ( O ` ( Q gsum ( x e. N |-> M ) ) ) ` Y ) = ( S gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) ) )
39 mpt0 
 |-  ( x e. (/) |-> M ) = (/)
40 39 a1i 
 |-  ( ph -> ( x e. (/) |-> M ) = (/) )
41 40 oveq2d 
 |-  ( ph -> ( Q gsum ( x e. (/) |-> M ) ) = ( Q gsum (/) ) )
42 41 fveq2d 
 |-  ( ph -> ( O ` ( Q gsum ( x e. (/) |-> M ) ) ) = ( O ` ( Q gsum (/) ) ) )
43 42 fveq1d 
 |-  ( ph -> ( ( O ` ( Q gsum ( x e. (/) |-> M ) ) ) ` Y ) = ( ( O ` ( Q gsum (/) ) ) ` Y ) )
44 mpt0 
 |-  ( x e. (/) |-> ( ( O ` M ) ` Y ) ) = (/)
45 44 a1i 
 |-  ( ph -> ( x e. (/) |-> ( ( O ` M ) ` Y ) ) = (/) )
46 45 oveq2d 
 |-  ( ph -> ( S gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) = ( S gsum (/) ) )
47 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
48 47 gsum0 
 |-  ( S gsum (/) ) = ( 0g ` S )
49 48 a1i 
 |-  ( ph -> ( S gsum (/) ) = ( 0g ` S ) )
50 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
51 6 50 ringidval 
 |-  ( 1r ` R ) = ( 0g ` S )
52 51 eqcomi 
 |-  ( 0g ` S ) = ( 1r ` R )
53 52 a1i 
 |-  ( ph -> ( 0g ` S ) = ( 1r ` R ) )
54 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
55 7 crngringd 
 |-  ( ph -> R e. Ring )
56 6 ringmgp 
 |-  ( R e. Ring -> S e. Mnd )
57 55 56 syl 
 |-  ( ph -> S e. Mnd )
58 eqid 
 |-  ( Base ` S ) = ( Base ` S )
59 58 47 mndidcl 
 |-  ( S e. Mnd -> ( 0g ` S ) e. ( Base ` S ) )
60 57 59 syl 
 |-  ( ph -> ( 0g ` S ) e. ( Base ` S ) )
61 eqid 
 |-  ( Base ` R ) = ( Base ` R )
62 6 61 mgpbas 
 |-  ( Base ` R ) = ( Base ` S )
63 4 62 eqtri 
 |-  B = ( Base ` S )
64 60 63 eleqtrrdi 
 |-  ( ph -> ( 0g ` S ) e. B )
65 51 a1i 
 |-  ( ph -> ( 1r ` R ) = ( 0g ` S ) )
66 65 eleq1d 
 |-  ( ph -> ( ( 1r ` R ) e. B <-> ( 0g ` S ) e. B ) )
67 64 66 mpbird 
 |-  ( ph -> ( 1r ` R ) e. B )
68 1 2 4 54 5 7 67 8 evl1scad 
 |-  ( ph -> ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. U /\ ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` Y ) = ( 1r ` R ) ) )
69 68 simprd 
 |-  ( ph -> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` Y ) = ( 1r ` R ) )
70 69 eqcomd 
 |-  ( ph -> ( 1r ` R ) = ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` Y ) )
71 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
72 2 54 50 71 ply1scl1 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
73 55 72 syl 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
74 3 71 ringidval 
 |-  ( 1r ` P ) = ( 0g ` Q )
75 74 a1i 
 |-  ( ph -> ( 1r ` P ) = ( 0g ` Q ) )
76 73 75 eqtrd 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 0g ` Q ) )
77 76 fveq2d 
 |-  ( ph -> ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( O ` ( 0g ` Q ) ) )
78 77 fveq1d 
 |-  ( ph -> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` Y ) = ( ( O ` ( 0g ` Q ) ) ` Y ) )
79 70 78 eqtrd 
 |-  ( ph -> ( 1r ` R ) = ( ( O ` ( 0g ` Q ) ) ` Y ) )
80 53 79 eqtrd 
 |-  ( ph -> ( 0g ` S ) = ( ( O ` ( 0g ` Q ) ) ` Y ) )
81 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
82 81 gsum0 
 |-  ( Q gsum (/) ) = ( 0g ` Q )
83 82 a1i 
 |-  ( ph -> ( Q gsum (/) ) = ( 0g ` Q ) )
84 83 eqcomd 
 |-  ( ph -> ( 0g ` Q ) = ( Q gsum (/) ) )
85 84 fveq2d 
 |-  ( ph -> ( O ` ( 0g ` Q ) ) = ( O ` ( Q gsum (/) ) ) )
86 85 fveq1d 
 |-  ( ph -> ( ( O ` ( 0g ` Q ) ) ` Y ) = ( ( O ` ( Q gsum (/) ) ) ` Y ) )
87 49 80 86 3eqtrd 
 |-  ( ph -> ( S gsum (/) ) = ( ( O ` ( Q gsum (/) ) ) ` Y ) )
88 46 87 eqtr2d 
 |-  ( ph -> ( ( O ` ( Q gsum (/) ) ) ` Y ) = ( S gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) )
89 43 88 eqtrd 
 |-  ( ph -> ( ( O ` ( Q gsum ( x e. (/) |-> M ) ) ) ` Y ) = ( S gsum ( x e. (/) |-> ( ( O ` M ) ` Y ) ) ) )
90 nfcv 
 |-  F/_ y M
91 nfcsb1v 
 |-  F/_ x [_ y / x ]_ M
92 csbeq1a 
 |-  ( x = y -> M = [_ y / x ]_ M )
93 90 91 92 cbvmpt 
 |-  ( x e. ( b u. { c } ) |-> M ) = ( y e. ( b u. { c } ) |-> [_ y / x ]_ M )
94 93 a1i 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( x e. ( b u. { c } ) |-> M ) = ( y e. ( b u. { c } ) |-> [_ y / x ]_ M ) )
95 94 oveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) = ( Q gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ M ) ) )
96 95 fveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( O ` ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) ) = ( O ` ( Q gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ M ) ) ) )
97 96 fveq1d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) ) ` Y ) = ( ( O ` ( Q gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ M ) ) ) ` Y ) )
98 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
99 eqid 
 |-  ( .r ` P ) = ( .r ` P )
100 3 99 mgpplusg 
 |-  ( .r ` P ) = ( +g ` Q )
101 2 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
102 7 101 syl 
 |-  ( ph -> P e. CRing )
103 3 crngmgp 
 |-  ( P e. CRing -> Q e. CMnd )
104 102 103 syl 
 |-  ( ph -> Q e. CMnd )
105 104 adantr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> Q e. CMnd )
106 105 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> Q e. CMnd )
107 10 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> N e. Fin )
108 simplrl 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> b C_ N )
109 107 108 ssfid 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> b e. Fin )
110 9 ad3antrrr 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> A. x e. N M e. U )
111 108 sselda 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> y e. N )
112 rspcsbela 
 |-  ( ( y e. N /\ A. x e. N M e. U ) -> [_ y / x ]_ M e. U )
113 112 expcom 
 |-  ( A. x e. N M e. U -> ( y e. N -> [_ y / x ]_ M e. U ) )
114 113 imp 
 |-  ( ( A. x e. N M e. U /\ y e. N ) -> [_ y / x ]_ M e. U )
115 110 111 114 syl2anc 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> [_ y / x ]_ M e. U )
116 3 5 mgpbas 
 |-  U = ( Base ` Q )
117 116 eqcomi 
 |-  ( Base ` Q ) = U
118 117 a1i 
 |-  ( ph -> ( Base ` Q ) = U )
119 118 adantr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( Base ` Q ) = U )
120 119 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( Base ` Q ) = U )
121 120 adantr 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> ( Base ` Q ) = U )
122 121 eleq2d 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> ( [_ y / x ]_ M e. ( Base ` Q ) <-> [_ y / x ]_ M e. U ) )
123 115 122 mpbird 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> [_ y / x ]_ M e. ( Base ` Q ) )
124 simplrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> c e. ( N \ b ) )
125 124 eldifbd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> -. c e. b )
126 124 eldifad 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> c e. N )
127 9 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> A. x e. N M e. U )
128 rspcsbela 
 |-  ( ( c e. N /\ A. x e. N M e. U ) -> [_ c / x ]_ M e. U )
129 126 127 128 syl2anc 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> [_ c / x ]_ M e. U )
130 120 eleq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( [_ c / x ]_ M e. ( Base ` Q ) <-> [_ c / x ]_ M e. U ) )
131 129 130 mpbird 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> [_ c / x ]_ M e. ( Base ` Q ) )
132 csbeq1 
 |-  ( y = c -> [_ y / x ]_ M = [_ c / x ]_ M )
133 98 100 106 109 123 124 125 131 132 gsumunsn 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( Q gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ M ) ) = ( ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) ( .r ` P ) [_ c / x ]_ M ) )
134 133 fveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( O ` ( Q gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ M ) ) ) = ( O ` ( ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) ( .r ` P ) [_ c / x ]_ M ) ) )
135 134 fveq1d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` ( Q gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ M ) ) ) ` Y ) = ( ( O ` ( ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) ( .r ` P ) [_ c / x ]_ M ) ) ` Y ) )
136 7 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> R e. CRing )
137 8 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> Y e. B )
138 115 ralrimiva 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> A. y e. b [_ y / x ]_ M e. U )
139 116 106 109 138 gsummptcl 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) e. U )
140 92 equcoms 
 |-  ( y = x -> M = [_ y / x ]_ M )
141 140 eqcomd 
 |-  ( y = x -> [_ y / x ]_ M = M )
142 91 90 141 cbvmpt 
 |-  ( y e. b |-> [_ y / x ]_ M ) = ( x e. b |-> M )
143 142 a1i 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( y e. b |-> [_ y / x ]_ M ) = ( x e. b |-> M ) )
144 143 oveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) = ( Q gsum ( x e. b |-> M ) ) )
145 144 fveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( O ` ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) ) = ( O ` ( Q gsum ( x e. b |-> M ) ) ) )
146 145 fveq1d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) ) ` Y ) = ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) )
147 139 146 jca 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) e. U /\ ( ( O ` ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) ) ` Y ) = ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) ) )
148 eqidd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` [_ c / x ]_ M ) ` Y ) = ( ( O ` [_ c / x ]_ M ) ` Y ) )
149 129 148 jca 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( [_ c / x ]_ M e. U /\ ( ( O ` [_ c / x ]_ M ) ` Y ) = ( ( O ` [_ c / x ]_ M ) ` Y ) ) )
150 eqid 
 |-  ( .r ` R ) = ( .r ` R )
151 1 2 4 5 136 137 147 149 99 150 evl1muld 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) ( .r ` P ) [_ c / x ]_ M ) e. U /\ ( ( O ` ( ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) ( .r ` P ) [_ c / x ]_ M ) ) ` Y ) = ( ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) ( .r ` R ) ( ( O ` [_ c / x ]_ M ) ` Y ) ) ) )
152 151 simprd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` ( ( Q gsum ( y e. b |-> [_ y / x ]_ M ) ) ( .r ` P ) [_ c / x ]_ M ) ) ` Y ) = ( ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) ( .r ` R ) ( ( O ` [_ c / x ]_ M ) ` Y ) ) )
153 135 152 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` ( Q gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ M ) ) ) ` Y ) = ( ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) ( .r ` R ) ( ( O ` [_ c / x ]_ M ) ` Y ) ) )
154 97 153 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) ) ` Y ) = ( ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) ( .r ` R ) ( ( O ` [_ c / x ]_ M ) ` Y ) ) )
155 6 150 mgpplusg 
 |-  ( .r ` R ) = ( +g ` S )
156 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
157 156 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
158 7 157 syl 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
159 6 158 eqeltrid 
 |-  ( ph -> S e. CMnd )
160 159 adantr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> S e. CMnd )
161 160 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> S e. CMnd )
162 csbfv12 
 |-  [_ y / x ]_ ( ( O ` M ) ` Y ) = ( [_ y / x ]_ ( O ` M ) ` [_ y / x ]_ Y )
163 csbfv2g 
 |-  ( y e. _V -> [_ y / x ]_ ( O ` M ) = ( O ` [_ y / x ]_ M ) )
164 163 elv 
 |-  [_ y / x ]_ ( O ` M ) = ( O ` [_ y / x ]_ M )
165 vex 
 |-  y e. _V
166 nfcv 
 |-  F/_ x Y
167 165 166 csbgfi 
 |-  [_ y / x ]_ Y = Y
168 164 167 fveq12i 
 |-  ( [_ y / x ]_ ( O ` M ) ` [_ y / x ]_ Y ) = ( ( O ` [_ y / x ]_ M ) ` Y )
169 162 168 eqtri 
 |-  [_ y / x ]_ ( ( O ` M ) ` Y ) = ( ( O ` [_ y / x ]_ M ) ` Y )
170 62 eqcomi 
 |-  ( Base ` S ) = ( Base ` R )
171 7 ad3antrrr 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> R e. CRing )
172 8 ad3antrrr 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> Y e. B )
173 63 eqcomi 
 |-  ( Base ` S ) = B
174 173 a1i 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> ( Base ` S ) = B )
175 174 eleq2d 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> ( Y e. ( Base ` S ) <-> Y e. B ) )
176 172 175 mpbird 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> Y e. ( Base ` S ) )
177 1 2 170 5 171 176 115 fveval1fvcl 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> ( ( O ` [_ y / x ]_ M ) ` Y ) e. ( Base ` S ) )
178 169 177 eqeltrid 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) /\ y e. b ) -> [_ y / x ]_ ( ( O ` M ) ` Y ) e. ( Base ` S ) )
179 1 2 4 5 136 137 129 fveval1fvcl 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` [_ c / x ]_ M ) ` Y ) e. B )
180 179 63 eleqtrdi 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` [_ c / x ]_ M ) ` Y ) e. ( Base ` S ) )
181 nfcv 
 |-  F/_ x c
182 nfcv 
 |-  F/_ x O
183 181 nfcsb1 
 |-  F/_ x [_ c / x ]_ M
184 182 183 nffv 
 |-  F/_ x ( O ` [_ c / x ]_ M )
185 184 166 nffv 
 |-  F/_ x ( ( O ` [_ c / x ]_ M ) ` Y )
186 csbeq1a 
 |-  ( x = c -> M = [_ c / x ]_ M )
187 186 fveq2d 
 |-  ( x = c -> ( O ` M ) = ( O ` [_ c / x ]_ M ) )
188 187 fveq1d 
 |-  ( x = c -> ( ( O ` M ) ` Y ) = ( ( O ` [_ c / x ]_ M ) ` Y ) )
189 181 185 188 csbhypf 
 |-  ( y = c -> [_ y / x ]_ ( ( O ` M ) ` Y ) = ( ( O ` [_ c / x ]_ M ) ` Y ) )
190 58 155 161 109 178 124 125 180 189 gsumunsn 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( S gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) ) = ( ( S gsum ( y e. b |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) ) ( .r ` R ) ( ( O ` [_ c / x ]_ M ) ` Y ) ) )
191 simpr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) )
192 nfcv 
 |-  F/_ y ( ( O ` M ) ` Y )
193 nfcsb1v 
 |-  F/_ x [_ y / x ]_ ( ( O ` M ) ` Y )
194 csbeq1a 
 |-  ( x = y -> ( ( O ` M ) ` Y ) = [_ y / x ]_ ( ( O ` M ) ` Y ) )
195 192 193 194 cbvmpt 
 |-  ( x e. b |-> ( ( O ` M ) ` Y ) ) = ( y e. b |-> [_ y / x ]_ ( ( O ` M ) ` Y ) )
196 195 a1i 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( x e. b |-> ( ( O ` M ) ` Y ) ) = ( y e. b |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) )
197 196 oveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) = ( S gsum ( y e. b |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) ) )
198 191 197 eqtr2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( S gsum ( y e. b |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) ) = ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) )
199 198 oveq1d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( S gsum ( y e. b |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) ) ( .r ` R ) ( ( O ` [_ c / x ]_ M ) ` Y ) ) = ( ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) ( .r ` R ) ( ( O ` [_ c / x ]_ M ) ` Y ) ) )
200 190 199 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( S gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) ) = ( ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) ( .r ` R ) ( ( O ` [_ c / x ]_ M ) ` Y ) ) )
201 200 eqcomd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) ( .r ` R ) ( ( O ` [_ c / x ]_ M ) ` Y ) ) = ( S gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) ) )
202 154 201 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) ) ` Y ) = ( S gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) ) )
203 192 193 194 cbvmpt 
 |-  ( x e. ( b u. { c } ) |-> ( ( O ` M ) ` Y ) ) = ( y e. ( b u. { c } ) |-> [_ y / x ]_ ( ( O ` M ) ` Y ) )
204 203 eqcomi 
 |-  ( y e. ( b u. { c } ) |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) = ( x e. ( b u. { c } ) |-> ( ( O ` M ) ` Y ) )
205 204 a1i 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( y e. ( b u. { c } ) |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) = ( x e. ( b u. { c } ) |-> ( ( O ` M ) ` Y ) ) )
206 205 oveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( S gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ ( ( O ` M ) ` Y ) ) ) = ( S gsum ( x e. ( b u. { c } ) |-> ( ( O ` M ) ` Y ) ) ) )
207 202 206 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) ) -> ( ( O ` ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) ) ` Y ) = ( S gsum ( x e. ( b u. { c } ) |-> ( ( O ` M ) ` Y ) ) ) )
208 207 ex 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( ( O ` ( Q gsum ( x e. b |-> M ) ) ) ` Y ) = ( S gsum ( x e. b |-> ( ( O ` M ) ` Y ) ) ) -> ( ( O ` ( Q gsum ( x e. ( b u. { c } ) |-> M ) ) ) ` Y ) = ( S gsum ( x e. ( b u. { c } ) |-> ( ( O ` M ) ` Y ) ) ) ) )
209 17 24 31 38 89 208 10 findcard2d 
 |-  ( ph -> ( ( O ` ( Q gsum ( x e. N |-> M ) ) ) ` Y ) = ( S gsum ( x e. N |-> ( ( O ` M ) ` Y ) ) ) )