Theorem mnringmulrcld 44465

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

Hypotheses

Ref	Expression
mnringmulrcld.2	⊢ 𝐹 = (𝑅 MndRing 𝑀)
mnringmulrcld.3	⊢ 𝐵 = (Base‘𝐹)
mnringmulrcld.1	⊢ 𝐴 = (Base‘𝑀)
mnringmulrcld.4	⊢ · = (.r‘𝐹)
mnringmulrcld.5	⊢ (𝜑 → 𝑅 ∈ Ring)
mnringmulrcld.6	⊢ (𝜑 → 𝑀 ∈ 𝑈)
mnringmulrcld.7	⊢ (𝜑 → 𝑋 ∈ 𝐵)
mnringmulrcld.8	⊢ (𝜑 → 𝑌 ∈ 𝐵)

Assertion

Ref	Expression
mnringmulrcld	⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)

Proof of Theorem mnringmulrcld

Dummy variables 𝑎 𝑏 𝑝 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mnringmulrcld.2	. . 3 ⊢ 𝐹 = (𝑅 MndRing 𝑀)
2		mnringmulrcld.3	. . 3 ⊢ 𝐵 = (Base‘𝐹)
3		eqid 2736	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
4		eqid 2736	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
5		mnringmulrcld.1	. . 3 ⊢ 𝐴 = (Base‘𝑀)
6		eqid 2736	. . 3 ⊢ (+g‘𝑀) = (+g‘𝑀)
7		mnringmulrcld.4	. . 3 ⊢ · = (.r‘𝐹)
8		mnringmulrcld.5	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
9		mnringmulrcld.6	. . 3 ⊢ (𝜑 → 𝑀 ∈ 𝑈)
10		mnringmulrcld.7	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
11		mnringmulrcld.8	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	mnringmulrvald 44464	. 2 ⊢ (𝜑 → (𝑋 · 𝑌) = (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))))
13		eqid 2736	. . 3 ⊢ (0g‘𝐹) = (0g‘𝐹)
14	1, 8, 9	mnringlmodd 44463	. . . 4 ⊢ (𝜑 → 𝐹 ∈ LMod)
15		lmodcmn 20861	. . . 4 ⊢ (𝐹 ∈ LMod → 𝐹 ∈ CMnd)
16	14, 15	syl 17	. . 3 ⊢ (𝜑 → 𝐹 ∈ CMnd)
17	5	fvexi 6848	. . . . 5 ⊢ 𝐴 ∈ V
18	17, 17	xpex 7698	. . . 4 ⊢ (𝐴 × 𝐴) ∈ V
19	18	a1i 11	. . 3 ⊢ (𝜑 → (𝐴 × 𝐴) ∈ V)
20	8	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑅 ∈ Ring)
21		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝑅) = (Base‘𝑅)
22	1, 2, 5, 21, 8, 9, 10	mnringbasefd 44455	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋:𝐴⟶(Base‘𝑅))
23	22	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑋:𝐴⟶(Base‘𝑅))
24		simp2 1137	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑎 ∈ 𝐴)
25	23, 24	ffvelcdmd 7030	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑋‘𝑎) ∈ (Base‘𝑅))
26	1, 2, 5, 21, 8, 9, 11	mnringbasefd 44455	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌:𝐴⟶(Base‘𝑅))
27	26	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑌:𝐴⟶(Base‘𝑅))
28		simp3 1138	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴)
29	27, 28	ffvelcdmd 7030	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑌‘𝑏) ∈ (Base‘𝑅))
30	21, 3	ringcl 20185	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑎) ∈ (Base‘𝑅) ∧ (𝑌‘𝑏) ∈ (Base‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) ∈ (Base‘𝑅))
31	20, 25, 29, 30	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) ∈ (Base‘𝑅))
32	21, 4	ring0cl 20202	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → (0g‘𝑅) ∈ (Base‘𝑅))
33	20, 32	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (0g‘𝑅) ∈ (Base‘𝑅))
34	31, 33	ifcld 4526	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)) ∈ (Base‘𝑅))
35	34	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑖 ∈ 𝐴) → if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)) ∈ (Base‘𝑅))
36	35	fmpttd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))):𝐴⟶(Base‘𝑅))
37	21	fvexi 6848	. . . . . . . . . 10 ⊢ (Base‘𝑅) ∈ V
38	37, 17	elmap 8809	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴) ↔ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))):𝐴⟶(Base‘𝑅))
39	36, 38	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴))
40	17	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝐴 ∈ V)
41		eqid 2736	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))
42	40, 33, 41	sniffsupp 9303	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) finSupp (0g‘𝑅))
43	39, 42	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴) ∧ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) finSupp (0g‘𝑅)))
44	9	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑀 ∈ 𝑈)
45	1, 2, 5, 21, 4, 20, 44	mnringelbased 44454	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵 ↔ ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴) ∧ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) finSupp (0g‘𝑅))))
46	43, 45	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵)
47	46	3expb 1120	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵)
48	47	ralrimivva 3179	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵)
49		eqid 2736	. . . . 5 ⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))
50	49	fmpo 8012	. . . 4 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵 ↔ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))):(𝐴 × 𝐴)⟶𝐵)
51	48, 50	sylib 218	. . 3 ⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))):(𝐴 × 𝐴)⟶𝐵)
52	17, 17	mpoex 8023	. . . . 5 ⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) ∈ V
53	52	a1i 11	. . . 4 ⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) ∈ V)
54	51	ffnd 6663	. . . 4 ⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) Fn (𝐴 × 𝐴))
55	13	fvexi 6848	. . . . 5 ⊢ (0g‘𝐹) ∈ V
56	55	a1i 11	. . . 4 ⊢ (𝜑 → (0g‘𝐹) ∈ V)
57	1, 2, 4, 8, 9, 10	mnringbasefsuppd 44456	. . . . . 6 ⊢ (𝜑 → 𝑋 finSupp (0g‘𝑅))
58	57	fsuppimpd 9272	. . . . 5 ⊢ (𝜑 → (𝑋 supp (0g‘𝑅)) ∈ Fin)
59	1, 2, 4, 8, 9, 11	mnringbasefsuppd 44456	. . . . . 6 ⊢ (𝜑 → 𝑌 finSupp (0g‘𝑅))
60	59	fsuppimpd 9272	. . . . 5 ⊢ (𝜑 → (𝑌 supp (0g‘𝑅)) ∈ Fin)
61		xpfi 9220	. . . . 5 ⊢ (((𝑋 supp (0g‘𝑅)) ∈ Fin ∧ (𝑌 supp (0g‘𝑅)) ∈ Fin) → ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∈ Fin)
62	58, 60, 61	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∈ Fin)
63		elxpi 5646	. . . . . . 7 ⊢ (𝑝 ∈ (𝐴 × 𝐴) → ∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)))
64		simpl 482	. . . . . . . 8 ⊢ ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑝 = ⟨𝑎, 𝑏⟩)
65	64	2eximi 1837	. . . . . . 7 ⊢ (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ∃𝑎∃𝑏 𝑝 = ⟨𝑎, 𝑏⟩)
66	63, 65	syl 17	. . . . . 6 ⊢ (𝑝 ∈ (𝐴 × 𝐴) → ∃𝑎∃𝑏 𝑝 = ⟨𝑎, 𝑏⟩)
67	66	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → ∃𝑎∃𝑏 𝑝 = ⟨𝑎, 𝑏⟩)
68		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑎(𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴))
69		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑎 𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅)))
70		nfmpo1 7438	. . . . . . . . 9 ⊢ Ⅎ𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))
71		nfcv 2898	. . . . . . . . 9 ⊢ Ⅎ𝑎𝑝
72	70, 71	nffv 6844	. . . . . . . 8 ⊢ Ⅎ𝑎((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝)
73		nfcv 2898	. . . . . . . 8 ⊢ Ⅎ𝑎(0g‘𝐹)
74	72, 73	nfeq 2912	. . . . . . 7 ⊢ Ⅎ𝑎((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)
75	69, 74	nfor 1905	. . . . . 6 ⊢ Ⅎ𝑎(𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))
76		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑏(𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴))
77		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑏 𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅)))
78		nfmpo2 7439	. . . . . . . . . 10 ⊢ Ⅎ𝑏(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))
79		nfcv 2898	. . . . . . . . . 10 ⊢ Ⅎ𝑏𝑝
80	78, 79	nffv 6844	. . . . . . . . 9 ⊢ Ⅎ𝑏((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝)
81		nfcv 2898	. . . . . . . . 9 ⊢ Ⅎ𝑏(0g‘𝐹)
82	80, 81	nfeq 2912	. . . . . . . 8 ⊢ Ⅎ𝑏((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)
83	77, 82	nfor 1905	. . . . . . 7 ⊢ Ⅎ𝑏(𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))
84		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝑝 = ⟨𝑎, 𝑏⟩)
85		simp2 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝑝 ∈ (𝐴 × 𝐴))
86	84, 85	eqeltrrd 2837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐴))
87		opelxp 5660	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐴) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))
88	86, 87	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))
89		ianor 983	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ↔ (¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∨ ¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅))))
90	22	ffnd 6663	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑋 Fn 𝐴)
91	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 ∈ V)
92	4	fvexi 6848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘𝑅) ∈ V
93	92	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (0g‘𝑅) ∈ V)
94		elsuppfn 8112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 Fn 𝐴 ∧ 𝐴 ∈ V ∧ (0g‘𝑅) ∈ V) → (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅))))
95	90, 91, 93, 94	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅))))
96	95	biimprd 248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)) → 𝑎 ∈ (𝑋 supp (0g‘𝑅))))
97	96	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)) → 𝑎 ∈ (𝑋 supp (0g‘𝑅))))
98	24, 97	mpand 695	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑋‘𝑎) ≠ (0g‘𝑅) → 𝑎 ∈ (𝑋 supp (0g‘𝑅))))
99	98	necon1bd 2950	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) → (𝑋‘𝑎) = (0g‘𝑅)))
100	26	ffnd 6663	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑌 Fn 𝐴)
101		elsuppfn 8112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑌 Fn 𝐴 ∧ 𝐴 ∈ V ∧ (0g‘𝑅) ∈ V) → (𝑏 ∈ (𝑌 supp (0g‘𝑅)) ↔ (𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅))))
102	100, 91, 93, 101	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑏 ∈ (𝑌 supp (0g‘𝑅)) ↔ (𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅))))
103	102	biimprd 248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)) → 𝑏 ∈ (𝑌 supp (0g‘𝑅))))
104	103	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)) → 𝑏 ∈ (𝑌 supp (0g‘𝑅))))
105	28, 104	mpand 695	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑌‘𝑏) ≠ (0g‘𝑅) → 𝑏 ∈ (𝑌 supp (0g‘𝑅))))
106	105	necon1bd 2950	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅)) → (𝑌‘𝑏) = (0g‘𝑅)))
107	99, 106	orim12d 966	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∨ ¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) → ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))))
108	107	imp 406	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ (¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∨ ¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) → ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅)))
109	89, 108	sylan2b 594	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) → ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅)))
110		oveq1 7365	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋‘𝑎) = (0g‘𝑅) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑏)))
111	21, 3, 4	ringlz 20228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑏) ∈ (Base‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅))
112	20, 29, 111	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅))
113	110, 112	sylan9eqr 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ (𝑋‘𝑎) = (0g‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅))
114		oveq2 7366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑌‘𝑏) = (0g‘𝑅) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = ((𝑋‘𝑎)(.r‘𝑅)(0g‘𝑅)))
115	21, 3, 4	ringrz 20229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑎) ∈ (Base‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
116	20, 25, 115	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑋‘𝑎)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
117	114, 116	sylan9eqr 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ (𝑌‘𝑏) = (0g‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅))
118	113, 117	jaodan 959	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅))
119	118	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) ∧ 𝑖 = (𝑎(+g‘𝑀)𝑏)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅))
120		eqidd 2737	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) ∧ ¬ 𝑖 = (𝑎(+g‘𝑀)𝑏)) → (0g‘𝑅) = (0g‘𝑅))
121	119, 120	ifeqda 4516	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)) = (0g‘𝑅))
122	121	mpteq2dv 5192	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)))
123		fconstmpt 5686	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 × {(0g‘𝑅)}) = (𝑖 ∈ 𝐴 ↦ (0g‘𝑅))
124	1, 4, 5, 8, 9	mnring0g2d 44459	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) = (0g‘𝐹))
125	123, 124	eqtr3id 2785	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)) = (0g‘𝐹))
126	125	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)) = (0g‘𝐹))
127	126	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)) = (0g‘𝐹))
128	122, 127	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))
129	109, 128	syldan 591	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))
130	129	ex 412	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)))
131	130	orrd 863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)))
132	131	3expb 1120	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)))
133	132	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)))
134		eleq1 2824	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ ⟨𝑎, 𝑏⟩ ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅)))))
135		opelxp 5660	. . . . . . . . . . . . 13 ⊢ (⟨𝑎, 𝑏⟩ ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))))
136	134, 135	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))))
137	136	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))))
138		simp2l 1200	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ 𝐴)
139		simp2r 1201	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝑏 ∈ 𝐴)
140		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))))
141		simp3 1138	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝑝 = ⟨𝑎, 𝑏⟩)
142	17	mptex 7169	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ V
143	142	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ V)
144	140, 141, 143	fvmpopr2d 7520	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))
145	138, 139, 144	mpd3an23 1465	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))
146	145	eqeq1d 2738	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹) ↔ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)))
147	137, 146	orbi12d 918	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ((𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)) ↔ ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))))
148	133, 147	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)))
149	88, 148	syld3an2 1413	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)))
150	149	3expia 1121	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))))
151	76, 83, 150	exlimd 2225	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (∃𝑏 𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))))
152	68, 75, 151	exlimd 2225	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (∃𝑎∃𝑏 𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))))
153	67, 152	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)))
154	53, 54, 56, 62, 153	finnzfsuppd 9276	. . 3 ⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) finSupp (0g‘𝐹))
155	2, 13, 16, 19, 51, 154	gsumcl 19844	. 2 ⊢ (𝜑 → (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))) ∈ 𝐵)
156	12, 155	eqeltrd 2836	1 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2932  ∀wral 3051  Vcvv 3440  ifcif 4479  {csn 4580  ⟨cop 4586   class class class wbr 5098   ↦ cmpt 5179   × cxp 5622   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492  (class class class)co 7358   ∈ cmpo 7360   supp csupp 8102   ↑_m cmap 8763  Fincfn 8883   finSupp cfsupp 9264  Basecbs 17136  +_gcplusg 17177  ._rcmulr 17178  0_gc0g 17359   Σ_g cgsu 17360  CMndccmn 19709  Ringcrg 20168  LModclmod 20811   MndRing cmnring 44448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-tp 4585  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-supp 8103  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-er 8635  df-map 8765  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9265  df-sup 9345  df-oi 9415  df-card 9851  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-2 12208  df-3 12209  df-4 12210  df-5 12211  df-6 12212  df-7 12213  df-8 12214  df-9 12215  df-n0 12402  df-z 12489  df-dec 12608  df-uz 12752  df-fz 13424  df-fzo 13571  df-seq 13925  df-hash 14254  df-struct 17074  df-sets 17091  df-slot 17109  df-ndx 17121  df-base 17137  df-ress 17158  df-plusg 17190  df-mulr 17191  df-sca 17193  df-vsca 17194  df-ip 17195  df-tset 17196  df-ple 17197  df-ds 17199  df-hom 17201  df-cco 17202  df-0g 17361  df-gsum 17362  df-prds 17367  df-pws 17369  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18866  df-minusg 18867  df-sbg 18868  df-subg 19053  df-cntz 19246  df-cmn 19711  df-abl 19712  df-mgp 20076  df-rng 20088  df-ur 20117  df-ring 20170  df-subrg 20503  df-lmod 20813  df-lss 20883  df-sra 21125  df-rgmod 21126  df-dsmm 21687  df-frlm 21702  df-mnring 44449

This theorem is referenced by: (None)