Metamath Proof Explorer

Theorem mnringmulrcld

Description: Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024)

Ref Expression
Hypotheses mnringmulrcld.2 
|- F = ( R MndRing M )
mnringmulrcld.3 
|- B = ( Base ` F )
mnringmulrcld.1 
|- A = ( Base ` M )
mnringmulrcld.4 
|- .x. = ( .r ` F )
mnringmulrcld.5 
|- ( ph -> R e. Ring )
mnringmulrcld.6 
|- ( ph -> M e. U )
mnringmulrcld.7 
|- ( ph -> X e. B )
mnringmulrcld.8 
|- ( ph -> Y e. B )
Assertion mnringmulrcld 
|- ( ph -> ( X .x. Y ) e. B )

Proof

Step Hyp Ref Expression
1 mnringmulrcld.2 
 |-  F = ( R MndRing M )
2 mnringmulrcld.3 
 |-  B = ( Base ` F )
3 mnringmulrcld.1 
 |-  A = ( Base ` M )
4 mnringmulrcld.4 
 |-  .x. = ( .r ` F )
5 mnringmulrcld.5 
 |-  ( ph -> R e. Ring )
6 mnringmulrcld.6 
 |-  ( ph -> M e. U )
7 mnringmulrcld.7 
 |-  ( ph -> X e. B )
8 mnringmulrcld.8 
 |-  ( ph -> Y e. B )
9 eqid 
 |-  ( .r ` R ) = ( .r ` R )
10 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
11 eqid 
 |-  ( +g ` M ) = ( +g ` M )
12 1 2 9 10 3 11 4 5 6 7 8 mnringmulrvald 
 |-  ( ph -> ( X .x. Y ) = ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ) )
13 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
14 1 5 6 mnringlmodd 
 |-  ( ph -> F e. LMod )
15 lmodcmn 
 |-  ( F e. LMod -> F e. CMnd )
16 14 15 syl 
 |-  ( ph -> F e. CMnd )
17 3 fvexi 
 |-  A e. _V
18 17 17 xpex 
 |-  ( A X. A ) e. _V
19 18 a1i 
 |-  ( ph -> ( A X. A ) e. _V )
20 5 3ad2ant1 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> R e. Ring )
21 eqid 
 |-  ( Base ` R ) = ( Base ` R )
22 1 2 3 21 5 6 7 mnringbasefd 
 |-  ( ph -> X : A --> ( Base ` R ) )
23 22 3ad2ant1 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> X : A --> ( Base ` R ) )
24 simp2 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> a e. A )
25 23 24 ffvelcdmd 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( X ` a ) e. ( Base ` R ) )
26 1 2 3 21 5 6 8 mnringbasefd 
 |-  ( ph -> Y : A --> ( Base ` R ) )
27 26 3ad2ant1 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> Y : A --> ( Base ` R ) )
28 simp3 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> b e. A )
29 27 28 ffvelcdmd 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( Y ` b ) e. ( Base ` R ) )
30 21 9 ringcl 
 |-  ( ( R e. Ring /\ ( X ` a ) e. ( Base ` R ) /\ ( Y ` b ) e. ( Base ` R ) ) -> ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) e. ( Base ` R ) )
31 20 25 29 30 syl3anc 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) e. ( Base ` R ) )
32 21 10 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
33 20 32 syl 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( 0g ` R ) e. ( Base ` R ) )
34 31 33 ifcld 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) e. ( Base ` R ) )
35 34 adantr 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ i e. A ) -> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) e. ( Base ` R ) )
36 35 fmpttd 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) : A --> ( Base ` R ) )
37 21 fvexi 
 |-  ( Base ` R ) e. _V
38 37 17 elmap 
 |-  ( ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m A ) <-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) : A --> ( Base ` R ) )
39 36 38 sylibr 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m A ) )
40 17 a1i 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> A e. _V )
41 eqid 
 |-  ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) )
42 40 33 41 sniffsupp 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) )
43 39 42 jca 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m A ) /\ ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) ) )
44 6 3ad2ant1 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> M e. U )
45 1 2 3 21 10 20 44 mnringelbased 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. B <-> ( ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m A ) /\ ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) ) ) )
46 43 45 mpbird 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. B )
47 46 3expb 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. B )
48 47 ralrimivva 
 |-  ( ph -> A. a e. A A. b e. A ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. B )
49 eqid 
 |-  ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) = ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) )
50 49 fmpo 
 |-  ( A. a e. A A. b e. A ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. B <-> ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) : ( A X. A ) --> B )
51 48 50 sylib 
 |-  ( ph -> ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) : ( A X. A ) --> B )
52 17 17 mpoex 
 |-  ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) e. _V
53 52 a1i 
 |-  ( ph -> ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) e. _V )
54 51 ffnd 
 |-  ( ph -> ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) Fn ( A X. A ) )
55 13 fvexi 
 |-  ( 0g ` F ) e. _V
56 55 a1i 
 |-  ( ph -> ( 0g ` F ) e. _V )
57 1 2 10 5 6 7 mnringbasefsuppd 
 |-  ( ph -> X finSupp ( 0g ` R ) )
58 57 fsuppimpd 
 |-  ( ph -> ( X supp ( 0g ` R ) ) e. Fin )
59 1 2 10 5 6 8 mnringbasefsuppd 
 |-  ( ph -> Y finSupp ( 0g ` R ) )
60 59 fsuppimpd 
 |-  ( ph -> ( Y supp ( 0g ` R ) ) e. Fin )
61 xpfi 
 |-  ( ( ( X supp ( 0g ` R ) ) e. Fin /\ ( Y supp ( 0g ` R ) ) e. Fin ) -> ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) e. Fin )
62 58 60 61 syl2anc 
 |-  ( ph -> ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) e. Fin )
63 elxpi 
 |-  ( p e. ( A X. A ) -> E. a E. b ( p = <. a , b >. /\ ( a e. A /\ b e. A ) ) )
64 simpl 
 |-  ( ( p = <. a , b >. /\ ( a e. A /\ b e. A ) ) -> p = <. a , b >. )
65 64 2eximi 
 |-  ( E. a E. b ( p = <. a , b >. /\ ( a e. A /\ b e. A ) ) -> E. a E. b p = <. a , b >. )
66 63 65 syl 
 |-  ( p e. ( A X. A ) -> E. a E. b p = <. a , b >. )
67 66 adantl 
 |-  ( ( ph /\ p e. ( A X. A ) ) -> E. a E. b p = <. a , b >. )
68 nfv 
 |-  F/ a ( ph /\ p e. ( A X. A ) )
69 nfv 
 |-  F/ a p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) )
70 nfmpo1 
 |-  F/_ a ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) )
71 nfcv 
 |-  F/_ a p
72 70 71 nffv 
 |-  F/_ a ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p )
73 nfcv 
 |-  F/_ a ( 0g ` F )
74 72 73 nfeq 
 |-  F/ a ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F )
75 69 74 nfor 
 |-  F/ a ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) \/ ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) )
76 nfv 
 |-  F/ b ( ph /\ p e. ( A X. A ) )
77 nfv 
 |-  F/ b p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) )
78 nfmpo2 
 |-  F/_ b ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) )
79 nfcv 
 |-  F/_ b p
80 78 79 nffv 
 |-  F/_ b ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p )
81 nfcv 
 |-  F/_ b ( 0g ` F )
82 80 81 nfeq 
 |-  F/ b ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F )
83 77 82 nfor 
 |-  F/ b ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) \/ ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) )
84 simp3 
 |-  ( ( ph /\ p e. ( A X. A ) /\ p = <. a , b >. ) -> p = <. a , b >. )
85 simp2 
 |-  ( ( ph /\ p e. ( A X. A ) /\ p = <. a , b >. ) -> p e. ( A X. A ) )
86 84 85 eqeltrrd 
 |-  ( ( ph /\ p e. ( A X. A ) /\ p = <. a , b >. ) -> <. a , b >. e. ( A X. A ) )
87 opelxp 
 |-  ( <. a , b >. e. ( A X. A ) <-> ( a e. A /\ b e. A ) )
88 86 87 sylib 
 |-  ( ( ph /\ p e. ( A X. A ) /\ p = <. a , b >. ) -> ( a e. A /\ b e. A ) )
89 ianor 
 |-  ( -. ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) <-> ( -. a e. ( X supp ( 0g ` R ) ) \/ -. b e. ( Y supp ( 0g ` R ) ) ) )
90 22 ffnd 
 |-  ( ph -> X Fn A )
91 17 a1i 
 |-  ( ph -> A e. _V )
92 10 fvexi 
 |-  ( 0g ` R ) e. _V
93 92 a1i 
 |-  ( ph -> ( 0g ` R ) e. _V )
94 elsuppfn 
 |-  ( ( X Fn A /\ A e. _V /\ ( 0g ` R ) e. _V ) -> ( a e. ( X supp ( 0g ` R ) ) <-> ( a e. A /\ ( X ` a ) =/= ( 0g ` R ) ) ) )
95 90 91 93 94 syl3anc 
 |-  ( ph -> ( a e. ( X supp ( 0g ` R ) ) <-> ( a e. A /\ ( X ` a ) =/= ( 0g ` R ) ) ) )
96 95 biimprd 
 |-  ( ph -> ( ( a e. A /\ ( X ` a ) =/= ( 0g ` R ) ) -> a e. ( X supp ( 0g ` R ) ) ) )
97 96 3ad2ant1 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( a e. A /\ ( X ` a ) =/= ( 0g ` R ) ) -> a e. ( X supp ( 0g ` R ) ) ) )
98 24 97 mpand 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( X ` a ) =/= ( 0g ` R ) -> a e. ( X supp ( 0g ` R ) ) ) )
99 98 necon1bd 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( -. a e. ( X supp ( 0g ` R ) ) -> ( X ` a ) = ( 0g ` R ) ) )
100 26 ffnd 
 |-  ( ph -> Y Fn A )
101 elsuppfn 
 |-  ( ( Y Fn A /\ A e. _V /\ ( 0g ` R ) e. _V ) -> ( b e. ( Y supp ( 0g ` R ) ) <-> ( b e. A /\ ( Y ` b ) =/= ( 0g ` R ) ) ) )
102 100 91 93 101 syl3anc 
 |-  ( ph -> ( b e. ( Y supp ( 0g ` R ) ) <-> ( b e. A /\ ( Y ` b ) =/= ( 0g ` R ) ) ) )
103 102 biimprd 
 |-  ( ph -> ( ( b e. A /\ ( Y ` b ) =/= ( 0g ` R ) ) -> b e. ( Y supp ( 0g ` R ) ) ) )
104 103 3ad2ant1 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( b e. A /\ ( Y ` b ) =/= ( 0g ` R ) ) -> b e. ( Y supp ( 0g ` R ) ) ) )
105 28 104 mpand 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( Y ` b ) =/= ( 0g ` R ) -> b e. ( Y supp ( 0g ` R ) ) ) )
106 105 necon1bd 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( -. b e. ( Y supp ( 0g ` R ) ) -> ( Y ` b ) = ( 0g ` R ) ) )
107 99 106 orim12d 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( -. a e. ( X supp ( 0g ` R ) ) \/ -. b e. ( Y supp ( 0g ` R ) ) ) -> ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) ) )
108 107 imp 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ ( -. a e. ( X supp ( 0g ` R ) ) \/ -. b e. ( Y supp ( 0g ` R ) ) ) ) -> ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) )
109 89 108 sylan2b 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ -. ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) ) -> ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) )
110 oveq1 
 |-  ( ( X ` a ) = ( 0g ` R ) -> ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) = ( ( 0g ` R ) ( .r ` R ) ( Y ` b ) ) )
111 21 9 10 ringlz 
 |-  ( ( R e. Ring /\ ( Y ` b ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) ( Y ` b ) ) = ( 0g ` R ) )
112 20 29 111 syl2anc 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( 0g ` R ) ( .r ` R ) ( Y ` b ) ) = ( 0g ` R ) )
113 110 112 sylan9eqr 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ ( X ` a ) = ( 0g ` R ) ) -> ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) = ( 0g ` R ) )
114 oveq2 
 |-  ( ( Y ` b ) = ( 0g ` R ) -> ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) = ( ( X ` a ) ( .r ` R ) ( 0g ` R ) ) )
115 21 9 10 ringrz 
 |-  ( ( R e. Ring /\ ( X ` a ) e. ( Base ` R ) ) -> ( ( X ` a ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
116 20 25 115 syl2anc 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( X ` a ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
117 114 116 sylan9eqr 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ ( Y ` b ) = ( 0g ` R ) ) -> ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) = ( 0g ` R ) )
118 113 117 jaodan 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) ) -> ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) = ( 0g ` R ) )
119 118 adantr 
 |-  ( ( ( ( ph /\ a e. A /\ b e. A ) /\ ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) ) /\ i = ( a ( +g ` M ) b ) ) -> ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) = ( 0g ` R ) )
120 eqidd 
 |-  ( ( ( ( ph /\ a e. A /\ b e. A ) /\ ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) ) /\ -. i = ( a ( +g ` M ) b ) ) -> ( 0g ` R ) = ( 0g ` R ) )
121 119 120 ifeqda 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) ) -> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) = ( 0g ` R ) )
122 121 mpteq2dv 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( i e. A |-> ( 0g ` R ) ) )
123 fconstmpt 
 |-  ( A X. { ( 0g ` R ) } ) = ( i e. A |-> ( 0g ` R ) )
124 1 10 3 5 6 mnring0g2d 
 |-  ( ph -> ( A X. { ( 0g ` R ) } ) = ( 0g ` F ) )
125 123 124 eqtr3id 
 |-  ( ph -> ( i e. A |-> ( 0g ` R ) ) = ( 0g ` F ) )
126 125 3ad2ant1 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( i e. A |-> ( 0g ` R ) ) = ( 0g ` F ) )
127 126 adantr 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) ) -> ( i e. A |-> ( 0g ` R ) ) = ( 0g ` F ) )
128 122 127 eqtrd 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ ( ( X ` a ) = ( 0g ` R ) \/ ( Y ` b ) = ( 0g ` R ) ) ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( 0g ` F ) )
129 109 128 syldan 
 |-  ( ( ( ph /\ a e. A /\ b e. A ) /\ -. ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( 0g ` F ) )
130 129 ex 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( -. ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( 0g ` F ) ) )
131 130 orrd 
 |-  ( ( ph /\ a e. A /\ b e. A ) -> ( ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) \/ ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( 0g ` F ) ) )
132 131 3expb 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) ) -> ( ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) \/ ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( 0g ` F ) ) )
133 132 3adant3 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> ( ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) \/ ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( 0g ` F ) ) )
134 eleq1 
 |-  ( p = <. a , b >. -> ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) <-> <. a , b >. e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) ) )
135 opelxp 
 |-  ( <. a , b >. e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) <-> ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) )
136 134 135 bitrdi 
 |-  ( p = <. a , b >. -> ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) <-> ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) ) )
137 136 3ad2ant3 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) <-> ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) ) )
138 simp2l 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> a e. A )
139 simp2r 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> b e. A )
140 eqidd 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) = ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) )
141 simp3 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> p = <. a , b >. )
142 17 mptex 
 |-  ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. _V
143 142 a1i 
 |-  ( ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) /\ a e. A /\ b e. A ) -> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) e. _V )
144 140 141 143 fvmpopr2d 
 |-  ( ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) /\ a e. A /\ b e. A ) -> ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) )
145 138 139 144 mpd3an23 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) )
146 145 eqeq1d 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> ( ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) <-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( 0g ` F ) ) )
147 137 146 orbi12d 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> ( ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) \/ ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) ) <-> ( ( a e. ( X supp ( 0g ` R ) ) /\ b e. ( Y supp ( 0g ` R ) ) ) \/ ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) = ( 0g ` F ) ) ) )
148 133 147 mpbird 
 |-  ( ( ph /\ ( a e. A /\ b e. A ) /\ p = <. a , b >. ) -> ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) \/ ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) ) )
149 88 148 syld3an2 
 |-  ( ( ph /\ p e. ( A X. A ) /\ p = <. a , b >. ) -> ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) \/ ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) ) )
150 149 3expia 
 |-  ( ( ph /\ p e. ( A X. A ) ) -> ( p = <. a , b >. -> ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) \/ ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) ) ) )
151 76 83 150 exlimd 
 |-  ( ( ph /\ p e. ( A X. A ) ) -> ( E. b p = <. a , b >. -> ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) \/ ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) ) ) )
152 68 75 151 exlimd 
 |-  ( ( ph /\ p e. ( A X. A ) ) -> ( E. a E. b p = <. a , b >. -> ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) \/ ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) ) ) )
153 67 152 mpd 
 |-  ( ( ph /\ p e. ( A X. A ) ) -> ( p e. ( ( X supp ( 0g ` R ) ) X. ( Y supp ( 0g ` R ) ) ) \/ ( ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ` p ) = ( 0g ` F ) ) )
154 53 54 56 62 153 finnzfsuppd 
 |-  ( ph -> ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) finSupp ( 0g ` F ) )
155 2 13 16 19 51 154 gsumcl 
 |-  ( ph -> ( F gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a ( +g ` M ) b ) , ( ( X ` a ) ( .r ` R ) ( Y ` b ) ) , ( 0g ` R ) ) ) ) ) e. B )
156 12 155 eqeltrd 
 |-  ( ph -> ( X .x. Y ) e. B )