Metamath Proof Explorer


Theorem mnringmulrcld

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

Ref Expression
Hypotheses mnringmulrcld.2 No typesetting found for |- F = ( R MndRing M ) with typecode |-
mnringmulrcld.3 B = Base F
mnringmulrcld.1 A = Base M
mnringmulrcld.4 · ˙ = F
mnringmulrcld.5 φ R Ring
mnringmulrcld.6 φ M U
mnringmulrcld.7 φ X B
mnringmulrcld.8 φ Y B
Assertion mnringmulrcld φ X · ˙ Y B

Proof

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