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

Metamath Proof Explorer

Theorem elrspunsn

Description: Membership to the span of an ideal R and a single element X . (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses elrspunidl.n 
|- N = ( RSpan ` R )
elrspunidl.b 
|- B = ( Base ` R )
elrspunidl.1 
|- .0. = ( 0g ` R )
elrspunidl.x 
|- .x. = ( .r ` R )
elrspunidl.r 
|- ( ph -> R e. Ring )
elrspunsn.p 
|- .+ = ( +g ` R )
elrspunsn.i 
|- ( ph -> I e. ( LIdeal ` R ) )
elrspunsn.x 
|- ( ph -> X e. ( B \ I ) )
Assertion elrspunsn 
|- ( ph -> ( A e. ( N ` ( I u. { X } ) ) <-> E. r e. B E. i e. I A = ( ( r .x. X ) .+ i ) ) )

Proof

Step Hyp Ref Expression
1 elrspunidl.n 
 |-  N = ( RSpan ` R )
2 elrspunidl.b 
 |-  B = ( Base ` R )
3 elrspunidl.1 
 |-  .0. = ( 0g ` R )
4 elrspunidl.x 
 |-  .x. = ( .r ` R )
5 elrspunidl.r 
 |-  ( ph -> R e. Ring )
6 elrspunsn.p 
 |-  .+ = ( +g ` R )
7 elrspunsn.i 
 |-  ( ph -> I e. ( LIdeal ` R ) )
8 elrspunsn.x 
 |-  ( ph -> X e. ( B \ I ) )
9 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
10 2 9 lidlss 
 |-  ( I e. ( LIdeal ` R ) -> I C_ B )
11 7 10 syl 
 |-  ( ph -> I C_ B )
12 8 eldifad 
 |-  ( ph -> X e. B )
13 12 snssd 
 |-  ( ph -> { X } C_ B )
14 11 13 unssd 
 |-  ( ph -> ( I u. { X } ) C_ B )
15 1 2 3 4 5 14 elrsp 
 |-  ( ph -> ( A e. ( N ` ( I u. { X } ) ) <-> E. a e. ( B ^m ( I u. { X } ) ) ( a finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) ) )
16 oveq1 
 |-  ( r = ( a ` X ) -> ( r .x. X ) = ( ( a ` X ) .x. X ) )
17 16 oveq1d 
 |-  ( r = ( a ` X ) -> ( ( r .x. X ) .+ i ) = ( ( ( a ` X ) .x. X ) .+ i ) )
18 17 eqeq2d 
 |-  ( r = ( a ` X ) -> ( A = ( ( r .x. X ) .+ i ) <-> A = ( ( ( a ` X ) .x. X ) .+ i ) ) )
19 oveq2 
 |-  ( i = ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) -> ( ( ( a ` X ) .x. X ) .+ i ) = ( ( ( a ` X ) .x. X ) .+ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) ) )
20 19 eqeq2d 
 |-  ( i = ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) -> ( A = ( ( ( a ` X ) .x. X ) .+ i ) <-> A = ( ( ( a ` X ) .x. X ) .+ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) ) ) )
21 elmapi 
 |-  ( a e. ( B ^m ( I u. { X } ) ) -> a : ( I u. { X } ) --> B )
22 21 ad3antlr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> a : ( I u. { X } ) --> B )
23 12 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> X e. B )
24 snidg 
 |-  ( X e. B -> X e. { X } )
25 elun2 
 |-  ( X e. { X } -> X e. ( I u. { X } ) )
26 23 24 25 3syl 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> X e. ( I u. { X } ) )
27 22 26 ffvelcdmd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( a ` X ) e. B )
28 2 fvexi 
 |-  B e. _V
29 28 a1i 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> B e. _V )
30 7 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> I e. ( LIdeal ` R ) )
31 ssun1 
 |-  I C_ ( I u. { X } )
32 31 a1i 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> I C_ ( I u. { X } ) )
33 22 32 fssresd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( a |` I ) : I --> B )
34 29 30 33 elmapdd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( a |` I ) e. ( B ^m I ) )
35 breq1 
 |-  ( b = ( a |` I ) -> ( b finSupp .0. <-> ( a |` I ) finSupp .0. ) )
36 fveq1 
 |-  ( b = ( a |` I ) -> ( b ` y ) = ( ( a |` I ) ` y ) )
37 36 oveq1d 
 |-  ( b = ( a |` I ) -> ( ( b ` y ) .x. y ) = ( ( ( a |` I ) ` y ) .x. y ) )
38 37 mpteq2dv 
 |-  ( b = ( a |` I ) -> ( y e. I |-> ( ( b ` y ) .x. y ) ) = ( y e. I |-> ( ( ( a |` I ) ` y ) .x. y ) ) )
39 38 oveq2d 
 |-  ( b = ( a |` I ) -> ( R gsum ( y e. I |-> ( ( b ` y ) .x. y ) ) ) = ( R gsum ( y e. I |-> ( ( ( a |` I ) ` y ) .x. y ) ) ) )
40 39 eqeq2d 
 |-  ( b = ( a |` I ) -> ( ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( b ` y ) .x. y ) ) ) <-> ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( ( a |` I ) ` y ) .x. y ) ) ) ) )
41 35 40 anbi12d 
 |-  ( b = ( a |` I ) -> ( ( b finSupp .0. /\ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( b ` y ) .x. y ) ) ) ) <-> ( ( a |` I ) finSupp .0. /\ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( ( a |` I ) ` y ) .x. y ) ) ) ) ) )
42 41 adantl 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) /\ b = ( a |` I ) ) -> ( ( b finSupp .0. /\ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( b ` y ) .x. y ) ) ) ) <-> ( ( a |` I ) finSupp .0. /\ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( ( a |` I ) ` y ) .x. y ) ) ) ) ) )
43 simplr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> a finSupp .0. )
44 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> R e. Ring )
45 2 3 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
46 44 45 syl 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> .0. e. B )
47 43 46 fsuppres 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( a |` I ) finSupp .0. )
48 fveq2 
 |-  ( x = y -> ( a ` x ) = ( a ` y ) )
49 id 
 |-  ( x = y -> x = y )
50 48 49 oveq12d 
 |-  ( x = y -> ( ( a ` x ) .x. x ) = ( ( a ` y ) .x. y ) )
51 50 cbvmptv 
 |-  ( x e. I |-> ( ( a ` x ) .x. x ) ) = ( y e. I |-> ( ( a ` y ) .x. y ) )
52 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) /\ y e. I ) -> y e. I )
53 52 fvresd 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) /\ y e. I ) -> ( ( a |` I ) ` y ) = ( a ` y ) )
54 53 oveq1d 
 |-  ( ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) /\ y e. I ) -> ( ( ( a |` I ) ` y ) .x. y ) = ( ( a ` y ) .x. y ) )
55 54 mpteq2dva 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( y e. I |-> ( ( ( a |` I ) ` y ) .x. y ) ) = ( y e. I |-> ( ( a ` y ) .x. y ) ) )
56 51 55 eqtr4id 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( x e. I |-> ( ( a ` x ) .x. x ) ) = ( y e. I |-> ( ( ( a |` I ) ` y ) .x. y ) ) )
57 56 oveq2d 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( ( a |` I ) ` y ) .x. y ) ) ) )
58 47 57 jca 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( ( a |` I ) finSupp .0. /\ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( ( a |` I ) ` y ) .x. y ) ) ) ) )
59 34 42 58 rspcedvd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> E. b e. ( B ^m I ) ( b finSupp .0. /\ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( b ` y ) .x. y ) ) ) ) )
60 11 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> I C_ B )
61 1 2 3 4 44 60 elrsp 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) e. ( N ` I ) <-> E. b e. ( B ^m I ) ( b finSupp .0. /\ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( y e. I |-> ( ( b ` y ) .x. y ) ) ) ) ) )
62 59 61 mpbird 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) e. ( N ` I ) )
63 1 9 rspidlid 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> ( N ` I ) = I )
64 5 7 63 syl2anc 
 |-  ( ph -> ( N ` I ) = I )
65 64 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( N ` I ) = I )
66 62 65 eleqtrd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) e. I )
67 simpr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) )
68 5 ringcmnd 
 |-  ( ph -> R e. CMnd )
69 68 ad2antrr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> R e. CMnd )
70 7 ad2antrr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> I e. ( LIdeal ` R ) )
71 snex 
 |-  { X } e. _V
72 71 a1i 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> { X } e. _V )
73 70 72 unexd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( I u. { X } ) e. _V )
74 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I u. { X } ) ) -> R e. Ring )
75 21 ad3antlr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I u. { X } ) ) -> a : ( I u. { X } ) --> B )
76 simpr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I u. { X } ) ) -> x e. ( I u. { X } ) )
77 75 76 ffvelcdmd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I u. { X } ) ) -> ( a ` x ) e. B )
78 14 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I u. { X } ) ) -> ( I u. { X } ) C_ B )
79 78 76 sseldd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I u. { X } ) ) -> x e. B )
80 2 4 74 77 79 ringcld 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I u. { X } ) ) -> ( ( a ` x ) .x. x ) e. B )
81 73 mptexd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) e. _V )
82 5 45 syl 
 |-  ( ph -> .0. e. B )
83 82 ad2antrr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> .0. e. B )
84 funmpt 
 |-  Fun ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) )
85 84 a1i 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> Fun ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) )
86 simpr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> a finSupp .0. )
87 86 fsuppimpd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( a supp .0. ) e. Fin )
88 21 ad3antlr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> a : ( I u. { X } ) --> B )
89 88 ffnd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> a Fn ( I u. { X } ) )
90 73 adantr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> ( I u. { X } ) e. _V )
91 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> R e. Ring )
92 91 45 syl 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> .0. e. B )
93 simpr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> x e. ( ( I u. { X } ) \ ( a supp .0. ) ) )
94 89 90 92 93 fvdifsupp 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> ( a ` x ) = .0. )
95 94 oveq1d 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> ( ( a ` x ) .x. x ) = ( .0. .x. x ) )
96 14 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> ( I u. { X } ) C_ B )
97 93 eldifad 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> x e. ( I u. { X } ) )
98 96 97 sseldd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> x e. B )
99 2 4 3 ringlz 
 |-  ( ( R e. Ring /\ x e. B ) -> ( .0. .x. x ) = .0. )
100 91 98 99 syl2anc 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> ( .0. .x. x ) = .0. )
101 95 100 eqtrd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( ( I u. { X } ) \ ( a supp .0. ) ) ) -> ( ( a ` x ) .x. x ) = .0. )
102 101 73 suppss2 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) supp .0. ) C_ ( a supp .0. ) )
103 87 102 ssfid 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) supp .0. ) e. Fin )
104 81 83 85 103 isfsuppd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) finSupp .0. )
105 8 eldifbd 
 |-  ( ph -> -. X e. I )
106 105 ad2antrr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> -. X e. I )
107 disjsn 
 |-  ( ( I i^i { X } ) = (/) <-> -. X e. I )
108 106 107 sylibr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( I i^i { X } ) = (/) )
109 eqidd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( I u. { X } ) = ( I u. { X } ) )
110 2 3 6 69 73 80 104 108 109 gsumsplit2 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) = ( ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) .+ ( R gsum ( x e. { X } |-> ( ( a ` x ) .x. x ) ) ) ) )
111 69 cmnmndd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> R e. Mnd )
112 12 ad2antrr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> X e. B )
113 5 ad2antrr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> R e. Ring )
114 21 ad2antlr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> a : ( I u. { X } ) --> B )
115 ssun2 
 |-  { X } C_ ( I u. { X } )
116 12 24 syl 
 |-  ( ph -> X e. { X } )
117 116 ad2antrr 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> X e. { X } )
118 115 117 sselid 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> X e. ( I u. { X } ) )
119 114 118 ffvelcdmd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( a ` X ) e. B )
120 2 4 113 119 112 ringcld 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( ( a ` X ) .x. X ) e. B )
121 simpr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x = X ) -> x = X )
122 121 fveq2d 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x = X ) -> ( a ` x ) = ( a ` X ) )
123 122 121 oveq12d 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x = X ) -> ( ( a ` x ) .x. x ) = ( ( a ` X ) .x. X ) )
124 2 111 112 120 123 gsumsnd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( R gsum ( x e. { X } |-> ( ( a ` x ) .x. x ) ) ) = ( ( a ` X ) .x. X ) )
125 124 oveq2d 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) .+ ( R gsum ( x e. { X } |-> ( ( a ` x ) .x. x ) ) ) ) = ( ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) .+ ( ( a ` X ) .x. X ) ) )
126 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. I ) -> R e. Ring )
127 21 ad3antlr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. I ) -> a : ( I u. { X } ) --> B )
128 simpr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. I ) -> x e. I )
129 31 128 sselid 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. I ) -> x e. ( I u. { X } ) )
130 127 129 ffvelcdmd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. I ) -> ( a ` x ) e. B )
131 11 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. I ) -> I C_ B )
132 131 128 sseldd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. I ) -> x e. B )
133 2 4 126 130 132 ringcld 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. I ) -> ( ( a ` x ) .x. x ) e. B )
134 133 fmpttd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( x e. I |-> ( ( a ` x ) .x. x ) ) : I --> B )
135 31 a1i 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> I C_ ( I u. { X } ) )
136 135 ssdifd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( I \ ( a supp .0. ) ) C_ ( ( I u. { X } ) \ ( a supp .0. ) ) )
137 136 sselda 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> x e. ( ( I u. { X } ) \ ( a supp .0. ) ) )
138 137 94 syldan 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> ( a ` x ) = .0. )
139 138 oveq1d 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> ( ( a ` x ) .x. x ) = ( .0. .x. x ) )
140 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> R e. Ring )
141 11 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> I C_ B )
142 simpr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> x e. ( I \ ( a supp .0. ) ) )
143 142 eldifad 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> x e. I )
144 141 143 sseldd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> x e. B )
145 140 144 99 syl2anc 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> ( .0. .x. x ) = .0. )
146 139 145 eqtrd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ x e. ( I \ ( a supp .0. ) ) ) -> ( ( a ` x ) .x. x ) = .0. )
147 146 70 suppss2 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( ( x e. I |-> ( ( a ` x ) .x. x ) ) supp .0. ) C_ ( a supp .0. ) )
148 87 147 ssfid 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( ( x e. I |-> ( ( a ` x ) .x. x ) ) supp .0. ) e. Fin )
149 2 3 69 70 134 148 gsumcl2 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) e. B )
150 2 6 cmncom 
 |-  ( ( R e. CMnd /\ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) e. B /\ ( ( a ` X ) .x. X ) e. B ) -> ( ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) .+ ( ( a ` X ) .x. X ) ) = ( ( ( a ` X ) .x. X ) .+ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) ) )
151 69 149 120 150 syl3anc 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) .+ ( ( a ` X ) .x. X ) ) = ( ( ( a ` X ) .x. X ) .+ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) ) )
152 110 125 151 3eqtrd 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) -> ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) = ( ( ( a ` X ) .x. X ) .+ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) ) )
153 152 adantr 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) = ( ( ( a ` X ) .x. X ) .+ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) ) )
154 67 153 eqtrd 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> A = ( ( ( a ` X ) .x. X ) .+ ( R gsum ( x e. I |-> ( ( a ` x ) .x. x ) ) ) ) )
155 18 20 27 66 154 2rspcedvdw 
 |-  ( ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ a finSupp .0. ) /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) -> E. r e. B E. i e. I A = ( ( r .x. X ) .+ i ) )
156 155 anasss 
 |-  ( ( ( ph /\ a e. ( B ^m ( I u. { X } ) ) ) /\ ( a finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) ) -> E. r e. B E. i e. I A = ( ( r .x. X ) .+ i ) )
157 156 r19.29an 
 |-  ( ( ph /\ E. a e. ( B ^m ( I u. { X } ) ) ( a finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) ) -> E. r e. B E. i e. I A = ( ( r .x. X ) .+ i ) )
158 28 a1i 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> B e. _V )
159 7 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> I e. ( LIdeal ` R ) )
160 71 a1i 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> { X } e. _V )
161 159 160 unexd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( I u. { X } ) e. _V )
162 simp-4r 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ y e. ( I u. { X } ) ) -> r e. B )
163 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
164 2 163 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
165 5 164 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
166 165 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ y e. ( I u. { X } ) ) -> ( 1r ` R ) e. B )
167 162 166 ifcld 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ y e. ( I u. { X } ) ) -> if ( y = X , r , ( 1r ` R ) ) e. B )
168 82 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ y e. ( I u. { X } ) ) -> .0. e. B )
169 167 168 ifcld 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ y e. ( I u. { X } ) ) -> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) e. B )
170 169 fmpttd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) : ( I u. { X } ) --> B )
171 158 161 170 elmapdd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) e. ( B ^m ( I u. { X } ) ) )
172 breq1 
 |-  ( a = ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) -> ( a finSupp .0. <-> ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) finSupp .0. ) )
173 fveq1 
 |-  ( a = ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) -> ( a ` x ) = ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) )
174 173 oveq1d 
 |-  ( a = ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) -> ( ( a ` x ) .x. x ) = ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) )
175 174 mpteq2dv 
 |-  ( a = ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) -> ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) = ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) )
176 175 oveq2d 
 |-  ( a = ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) -> ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) = ( R gsum ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) )
177 176 eqeq2d 
 |-  ( a = ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) -> ( A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) <-> A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) ) )
178 172 177 anbi12d 
 |-  ( a = ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) -> ( ( a finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) <-> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) ) ) )
179 178 adantl 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ a = ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ) -> ( ( a finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) <-> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) ) ) )
180 eqid 
 |-  ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) = ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) )
181 prfi 
 |-  { X , i } e. Fin
182 181 a1i 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> { X , i } e. Fin )
183 simp-4r 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ y e. { X , i } ) -> r e. B )
184 165 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ y e. { X , i } ) -> ( 1r ` R ) e. B )
185 183 184 ifcld 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ y e. { X , i } ) -> if ( y = X , r , ( 1r ` R ) ) e. B )
186 82 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> .0. e. B )
187 180 161 182 185 186 mptiffisupp 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) finSupp .0. )
188 68 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> R e. CMnd )
189 159 10 syl 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> I C_ B )
190 simplr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> i e. I )
191 189 190 sseldd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> i e. B )
192 5 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> R e. Ring )
193 simpllr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> r e. B )
194 12 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> X e. B )
195 2 4 192 193 194 ringcld 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( r .x. X ) e. B )
196 2 6 cmncom 
 |-  ( ( R e. CMnd /\ i e. B /\ ( r .x. X ) e. B ) -> ( i .+ ( r .x. X ) ) = ( ( r .x. X ) .+ i ) )
197 188 191 195 196 syl3anc 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( i .+ ( r .x. X ) ) = ( ( r .x. X ) .+ i ) )
198 188 cmnmndd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> R e. Mnd )
199 eqid 
 |-  ( x e. I |-> if ( x = i , i , .0. ) ) = ( x e. I |-> if ( x = i , i , .0. ) )
200 191 2 eleqtrdi 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> i e. ( Base ` R ) )
201 3 198 159 190 199 200 gsummptif1n0 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( R gsum ( x e. I |-> if ( x = i , i , .0. ) ) ) = i )
202 fveq2 
 |-  ( x = i -> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) = ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` i ) )
203 id 
 |-  ( x = i -> x = i )
204 202 203 oveq12d 
 |-  ( x = i -> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) = ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` i ) .x. i ) )
205 204 adantl 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) = ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` i ) .x. i ) )
206 simpr 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> y = i )
207 prid2g 
 |-  ( i e. I -> i e. { X , i } )
208 207 ad5antlr 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> i e. { X , i } )
209 206 208 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> y e. { X , i } )
210 209 iftrued 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) = if ( y = X , r , ( 1r ` R ) ) )
211 190 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> i e. I )
212 211 adantr 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> i e. I )
213 206 212 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> y e. I )
214 105 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> -. X e. I )
215 214 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> -. X e. I )
216 nelneq 
 |-  ( ( y e. I /\ -. X e. I ) -> -. y = X )
217 213 215 216 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> -. y = X )
218 217 iffalsed 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> if ( y = X , r , ( 1r ` R ) ) = ( 1r ` R ) )
219 210 218 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) /\ y = i ) -> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) = ( 1r ` R ) )
220 31 211 sselid 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> i e. ( I u. { X } ) )
221 192 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> R e. Ring )
222 221 164 syl 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> ( 1r ` R ) e. B )
223 180 219 220 222 fvmptd2 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` i ) = ( 1r ` R ) )
224 223 oveq1d 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` i ) .x. i ) = ( ( 1r ` R ) .x. i ) )
225 191 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> i e. B )
226 2 4 163 221 225 ringlidmd 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> ( ( 1r ` R ) .x. i ) = i )
227 205 224 226 3eqtrrd 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ x = i ) -> i = ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) )
228 eleq1w 
 |-  ( y = x -> ( y e. { X , i } <-> x e. { X , i } ) )
229 eqeq1 
 |-  ( y = x -> ( y = X <-> x = X ) )
230 229 ifbid 
 |-  ( y = x -> if ( y = X , r , ( 1r ` R ) ) = if ( x = X , r , ( 1r ` R ) ) )
231 228 230 ifbieq1d 
 |-  ( y = x -> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) = if ( x e. { X , i } , if ( x = X , r , ( 1r ` R ) ) , .0. ) )
232 simplr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> x e. I )
233 31 232 sselid 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> x e. ( I u. { X } ) )
234 193 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> r e. B )
235 165 ad5antr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> ( 1r ` R ) e. B )
236 234 235 ifcld 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> if ( x = X , r , ( 1r ` R ) ) e. B )
237 186 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> .0. e. B )
238 236 237 ifcld 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> if ( x e. { X , i } , if ( x = X , r , ( 1r ` R ) ) , .0. ) e. B )
239 180 231 233 238 fvmptd3 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) = if ( x e. { X , i } , if ( x = X , r , ( 1r ` R ) ) , .0. ) )
240 214 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> -. X e. I )
241 nelne2 
 |-  ( ( x e. I /\ -. X e. I ) -> x =/= X )
242 232 240 241 syl2anc 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> x =/= X )
243 neqne 
 |-  ( -. x = i -> x =/= i )
244 243 adantl 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> x =/= i )
245 242 244 nelprd 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> -. x e. { X , i } )
246 245 iffalsed 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> if ( x e. { X , i } , if ( x = X , r , ( 1r ` R ) ) , .0. ) = .0. )
247 239 246 eqtrd 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) = .0. )
248 247 oveq1d 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) = ( .0. .x. x ) )
249 192 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> R e. Ring )
250 189 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> I C_ B )
251 250 232 sseldd 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> x e. B )
252 249 251 99 syl2anc 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> ( .0. .x. x ) = .0. )
253 248 252 eqtr2d 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) /\ -. x = i ) -> .0. = ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) )
254 227 253 ifeqda 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. I ) -> if ( x = i , i , .0. ) = ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) )
255 254 mpteq2dva 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( x e. I |-> if ( x = i , i , .0. ) ) = ( x e. I |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) )
256 255 oveq2d 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( R gsum ( x e. I |-> if ( x = i , i , .0. ) ) ) = ( R gsum ( x e. I |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) )
257 201 256 eqtr3d 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> i = ( R gsum ( x e. I |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) )
258 simpr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> y = x )
259 simplr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> x = X )
260 194 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> X e. B )
261 prid1g 
 |-  ( X e. B -> X e. { X , i } )
262 260 261 syl 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> X e. { X , i } )
263 259 262 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> x e. { X , i } )
264 258 263 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> y e. { X , i } )
265 264 iftrued 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) = if ( y = X , r , ( 1r ` R ) ) )
266 258 259 eqtrd 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> y = X )
267 266 iftrued 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> if ( y = X , r , ( 1r ` R ) ) = r )
268 265 267 eqtrd 
 |-  ( ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) /\ y = x ) -> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) = r )
269 simpr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) -> x = X )
270 116 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) -> X e. { X } )
271 270 25 syl 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) -> X e. ( I u. { X } ) )
272 269 271 eqeltrd 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) -> x e. ( I u. { X } ) )
273 193 adantr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) -> r e. B )
274 180 268 272 273 fvmptd2 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) -> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) = r )
275 274 269 oveq12d 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x = X ) -> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) = ( r .x. X ) )
276 2 198 194 195 275 gsumsnd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( R gsum ( x e. { X } |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) = ( r .x. X ) )
277 276 eqcomd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( r .x. X ) = ( R gsum ( x e. { X } |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) )
278 257 277 oveq12d 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( i .+ ( r .x. X ) ) = ( ( R gsum ( x e. I |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) .+ ( R gsum ( x e. { X } |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) ) )
279 197 278 eqtr3d 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( ( r .x. X ) .+ i ) = ( ( R gsum ( x e. I |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) .+ ( R gsum ( x e. { X } |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) ) )
280 simpr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> A = ( ( r .x. X ) .+ i ) )
281 5 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( I u. { X } ) ) -> R e. Ring )
282 170 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( I u. { X } ) ) -> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) e. B )
283 14 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( I u. { X } ) ) -> ( I u. { X } ) C_ B )
284 simpr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( I u. { X } ) ) -> x e. ( I u. { X } ) )
285 283 284 sseldd 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( I u. { X } ) ) -> x e. B )
286 2 4 281 282 285 ringcld 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( I u. { X } ) ) -> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) e. B )
287 161 mptexd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) e. _V )
288 funmpt 
 |-  Fun ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) )
289 288 a1i 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> Fun ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) )
290 187 fsuppimpd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) e. Fin )
291 nfv 
 |-  F/ y ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) )
292 291 169 180 fnmptd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) Fn ( I u. { X } ) )
293 292 adantr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) Fn ( I u. { X } ) )
294 161 adantr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> ( I u. { X } ) e. _V )
295 186 adantr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> .0. e. B )
296 simpr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) )
297 293 294 295 296 fvdifsupp 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) = .0. )
298 297 oveq1d 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) = ( .0. .x. x ) )
299 5 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> R e. Ring )
300 14 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> ( I u. { X } ) C_ B )
301 296 eldifad 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> x e. ( I u. { X } ) )
302 300 301 sseldd 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> x e. B )
303 299 302 99 syl2anc 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> ( .0. .x. x ) = .0. )
304 298 303 eqtrd 
 |-  ( ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) /\ x e. ( ( I u. { X } ) \ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) ) ) -> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) = .0. )
305 304 161 suppss2 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) supp .0. ) C_ ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) supp .0. ) )
306 290 305 ssfid 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) supp .0. ) e. Fin )
307 287 186 289 306 isfsuppd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) finSupp .0. )
308 214 107 sylibr 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( I i^i { X } ) = (/) )
309 eqidd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( I u. { X } ) = ( I u. { X } ) )
310 2 3 6 188 161 286 307 308 309 gsumsplit2 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( R gsum ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) = ( ( R gsum ( x e. I |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) .+ ( R gsum ( x e. { X } |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) ) )
311 279 280 310 3eqtr4d 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) )
312 187 311 jca 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( ( y e. ( I u. { X } ) |-> if ( y e. { X , i } , if ( y = X , r , ( 1r ` R ) ) , .0. ) ) ` x ) .x. x ) ) ) ) )
313 171 179 312 rspcedvd 
 |-  ( ( ( ( ph /\ r e. B ) /\ i e. I ) /\ A = ( ( r .x. X ) .+ i ) ) -> E. a e. ( B ^m ( I u. { X } ) ) ( a finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) )
314 313 r19.29ffa 
 |-  ( ( ph /\ E. r e. B E. i e. I A = ( ( r .x. X ) .+ i ) ) -> E. a e. ( B ^m ( I u. { X } ) ) ( a finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) )
315 157 314 impbida 
 |-  ( ph -> ( E. a e. ( B ^m ( I u. { X } ) ) ( a finSupp .0. /\ A = ( R gsum ( x e. ( I u. { X } ) |-> ( ( a ` x ) .x. x ) ) ) ) <-> E. r e. B E. i e. I A = ( ( r .x. X ) .+ i ) ) )
316 15 315 bitrd 
 |-  ( ph -> ( A e. ( N ` ( I u. { X } ) ) <-> E. r e. B E. i e. I A = ( ( r .x. X ) .+ i ) ) )