qusmul

Description: Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024)

	Ref	Expression
Hypotheses	qusmul.h	⊢ 𝑄 = ( 𝑅 /_s ( 𝑅 ~_QG 𝐼 ) )
	qusmul.v	⊢ 𝐵 = ( Base ‘ 𝑅 )
	qusmul.p	⊢ · = ( ._r ‘ 𝑅 )
	qusmul.a	⊢ × = ( ._r ‘ 𝑄 )
	qusmul.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	qusmul.i	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
	qusmul.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	qusmul.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	qusmul	⊢ ( 𝜑 → ( [ 𝑋 ] ( 𝑅 ~_QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~_QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~_QG 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		qusmul.h	⊢ 𝑄 = ( 𝑅 /_s ( 𝑅 ~_QG 𝐼 ) )
2		qusmul.v	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		qusmul.p	⊢ · = ( ._r ‘ 𝑅 )
4		qusmul.a	⊢ × = ( ._r ‘ 𝑄 )
5		qusmul.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		qusmul.i	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
7		qusmul.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		qusmul.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9	1	a1i	⊢ ( 𝜑 → 𝑄 = ( 𝑅 /_s ( 𝑅 ~_QG 𝐼 ) ) )
10	2	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
11	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
12		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
13	12	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
14	11 6 13	syl2anc	⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
15		eqid	⊢ ( 𝑅 ~_QG 𝐼 ) = ( 𝑅 ~_QG 𝐼 )
16	2 15	eqger	⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~_QG 𝐼 ) Er 𝐵 )
17	14 16	syl	⊢ ( 𝜑 → ( 𝑅 ~_QG 𝐼 ) Er 𝐵 )
18	12	crng2idl	⊢ ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
19	5 18	syl	⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
20	6 19	eleqtrd	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
21		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
22	2 15 21 3	2idlcpbl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) → ( ( 𝑥 ( 𝑅 ~_QG 𝐼 ) 𝑦 ∧ 𝑧 ( 𝑅 ~_QG 𝐼 ) 𝑡 ) → ( 𝑥 · 𝑧 ) ( 𝑅 ~_QG 𝐼 ) ( 𝑦 · 𝑡 ) ) )
23	11 20 22	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ( 𝑅 ~_QG 𝐼 ) 𝑦 ∧ 𝑧 ( 𝑅 ~_QG 𝐼 ) 𝑡 ) → ( 𝑥 · 𝑧 ) ( 𝑅 ~_QG 𝐼 ) ( 𝑦 · 𝑡 ) ) )
24	2 3	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑝 · 𝑞 ) ∈ 𝐵 )
25	24	3expb	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝐵 )
26	11 25	sylan	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝐵 )
27	26	caovclg	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ) → ( 𝑦 · 𝑡 ) ∈ 𝐵 )
28	9 10 17 5 23 27 3 4	qusmulval	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( [ 𝑋 ] ( 𝑅 ~_QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~_QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~_QG 𝐼 ) )
29	7 8 28	mpd3an23	⊢ ( 𝜑 → ( [ 𝑋 ] ( 𝑅 ~_QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~_QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~_QG 𝐼 ) )

Metamath Proof Explorer

Theorem qusmul

Proof