Theorem mnringmulrcld

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

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

Proof

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