qusmul2idl

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

	Ref	Expression
Hypotheses	qusmul2idl.h	⊢ 𝑄 = ( 𝑅 /_s ( 𝑅 ~_QG 𝐼 ) )
	qusmul2idl.v	⊢ 𝐵 = ( Base ‘ 𝑅 )
	qusmul2idl.p	⊢ · = ( ._r ‘ 𝑅 )
	qusmul2idl.a	⊢ × = ( ._r ‘ 𝑄 )
	qusmul2idl.1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	qusmul2idl.2	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	qusmul2idl.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	qusmul2idl.4	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	qusmul2idl	⊢ ( 𝜑 → ( [ 𝑋 ] ( 𝑅 ~_QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~_QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~_QG 𝐼 ) )

Proof

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

Metamath Proof Explorer

Theorem qusmul2idl

Proof