opprqusmulr

Description: The multiplication operation of the quotient of the opposite ring is the same as the multiplication operation of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

	Ref	Expression
Hypotheses	opprqus.b	$⊢ B = {Base}_{R}$
	opprqus.o	$⊢ O = {opp}_{r} (R)$
	opprqus.q	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
	opprqus1r.r	$⊢ φ \to R \in Ring$
	opprqus1r.i	$⊢ φ \to I \in 2Ideal (R)$
	opprqusmulr.e	$⊢ E = {Base}_{Q}$
	opprqusmulr.x	$⊢ φ \to X \in E$
	opprqusmulr.y	$⊢ φ \to Y \in E$
Assertion	opprqusmulr	$⊢ φ \to X \cdot_{{opp}_{r} (Q)} Y = X \cdot_{(O /_{𝑠} (O ~_{QG} I))} Y$

Proof

Step	Hyp	Ref	Expression
1		opprqus.b	$⊢ B = {Base}_{R}$
2		opprqus.o	$⊢ O = {opp}_{r} (R)$
3		opprqus.q	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
4		opprqus1r.r	$⊢ φ \to R \in Ring$
5		opprqus1r.i	$⊢ φ \to I \in 2Ideal (R)$
6		opprqusmulr.e	$⊢ E = {Base}_{Q}$
7		opprqusmulr.x	$⊢ φ \to X \in E$
8		opprqusmulr.y	$⊢ φ \to Y \in E$
9		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
10		eqid	$⊢ {opp}_{r} (Q) = {opp}_{r} (Q)$
11		eqid	$⊢ \cdot_{{opp}_{r} (Q)} = \cdot_{{opp}_{r} (Q)}$
12	6 9 10 11	opprmul	$⊢ X \cdot_{{opp}_{r} (Q)} Y = Y \cdot_{Q} X$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14	4	ad4antr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to R \in Ring$
15	5	ad4antr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to I \in 2Ideal (R)$
16		simplr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to q \in B$
17		simp-4r	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to p \in B$
18	3 1 13 9 14 15 16 17	qusmul2	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to [q] (R ~_{QG} I) \cdot_{Q} [p] (R ~_{QG} I) = [(q \cdot_{R} p)] (R ~_{QG} I)$
19		simpr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to Y = [q] (R ~_{QG} I)$
20		simpllr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to X = [p] (R ~_{QG} I)$
21	19 20	oveq12d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to Y \cdot_{Q} X = [q] (R ~_{QG} I) \cdot_{Q} [p] (R ~_{QG} I)$
22		eqid	$⊢ O /_{𝑠} (O ~_{QG} I) = O /_{𝑠} (O ~_{QG} I)$
23	2 1	opprbas	$⊢ B = {Base}_{O}$
24		eqid	$⊢ \cdot_{O} = \cdot_{O}$
25		eqid	$⊢ \cdot_{(O /_{𝑠} (O ~_{QG} I))} = \cdot_{(O /_{𝑠} (O ~_{QG} I))}$
26	2	opprring	$⊢ R \in Ring \to O \in Ring$
27	4 26	syl	$⊢ φ \to O \in Ring$
28	27	ad4antr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to O \in Ring$
29	2 4	oppr2idl	$⊢ φ \to 2Ideal (R) = 2Ideal (O)$
30	5 29	eleqtrd	$⊢ φ \to I \in 2Ideal (O)$
31	30	ad4antr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to I \in 2Ideal (O)$
32	22 23 24 25 28 31 17 16	qusmul2	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to [p] (O ~_{QG} I) \cdot_{(O /_{𝑠} (O ~_{QG} I))} [q] (O ~_{QG} I) = [(p \cdot_{O} q)] (O ~_{QG} I)$
33	5	2idllidld	$⊢ φ \to I \in LIdeal (R)$
34		eqid	$⊢ LIdeal (R) = LIdeal (R)$
35	1 34	lidlss	$⊢ I \in LIdeal (R) \to I \subseteq B$
36	33 35	syl	$⊢ φ \to I \subseteq B$
37	2 1	oppreqg	$⊢ (R \in Ring \land I \subseteq B) \to R ~_{QG} I = O ~_{QG} I$
38	4 36 37	syl2anc	$⊢ φ \to R ~_{QG} I = O ~_{QG} I$
39	38	ad4antr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to R ~_{QG} I = O ~_{QG} I$
40	39	eceq2d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to [p] (R ~_{QG} I) = [p] (O ~_{QG} I)$
41	20 40	eqtrd	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to X = [p] (O ~_{QG} I)$
42	39	eceq2d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to [q] (R ~_{QG} I) = [q] (O ~_{QG} I)$
43	19 42	eqtrd	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to Y = [q] (O ~_{QG} I)$
44	41 43	oveq12d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to X \cdot_{(O /_{𝑠} (O ~_{QG} I))} Y = [p] (O ~_{QG} I) \cdot_{(O /_{𝑠} (O ~_{QG} I))} [q] (O ~_{QG} I)$
45	1 13 2 24	opprmul	$⊢ p \cdot_{O} q = q \cdot_{R} p$
46	45	a1i	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to p \cdot_{O} q = q \cdot_{R} p$
47	46	eceq1d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to [(p \cdot_{O} q)] (R ~_{QG} I) = [(q \cdot_{R} p)] (R ~_{QG} I)$
48	39	eceq2d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to [(p \cdot_{O} q)] (R ~_{QG} I) = [(p \cdot_{O} q)] (O ~_{QG} I)$
49	47 48	eqtr3d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to [(q \cdot_{R} p)] (R ~_{QG} I) = [(p \cdot_{O} q)] (O ~_{QG} I)$
50	32 44 49	3eqtr4d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to X \cdot_{(O /_{𝑠} (O ~_{QG} I))} Y = [(q \cdot_{R} p)] (R ~_{QG} I)$
51	18 21 50	3eqtr4d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to Y \cdot_{Q} X = X \cdot_{(O /_{𝑠} (O ~_{QG} I))} Y$
52	10 6	opprbas	$⊢ E = {Base}_{{opp}_{r} (Q)}$
53	8 52	eleqtrdi	$⊢ φ \to Y \in {Base}_{{opp}_{r} (Q)}$
54	53	ad2antrr	$⊢ ((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \to Y \in {Base}_{{opp}_{r} (Q)}$
55	3	a1i	$⊢ φ \to Q = R /_{𝑠} (R ~_{QG} I)$
56	1	a1i	$⊢ φ \to B = {Base}_{R}$
57		ovexd	$⊢ φ \to R ~_{QG} I \in V$
58	55 56 57 4	qusbas	$⊢ φ \to B / (R ~_{QG} I) = {Base}_{Q}$
59	6 52	eqtr3i	$⊢ {Base}_{Q} = {Base}_{{opp}_{r} (Q)}$
60	58 59	eqtr2di	$⊢ φ \to {Base}_{{opp}_{r} (Q)} = B / (R ~_{QG} I)$
61	60	ad2antrr	$⊢ ((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \to {Base}_{{opp}_{r} (Q)} = B / (R ~_{QG} I)$
62	54 61	eleqtrd	$⊢ ((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \to Y \in (B / (R ~_{QG} I))$
63		elqsi	$⊢ Y \in (B / (R ~_{QG} I)) \to \exists q \in B Y = [q] (R ~_{QG} I)$
64	62 63	syl	$⊢ ((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \to \exists q \in B Y = [q] (R ~_{QG} I)$
65	51 64	r19.29a	$⊢ ((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \to Y \cdot_{Q} X = X \cdot_{(O /_{𝑠} (O ~_{QG} I))} Y$
66	7 52	eleqtrdi	$⊢ φ \to X \in {Base}_{{opp}_{r} (Q)}$
67	66 60	eleqtrd	$⊢ φ \to X \in (B / (R ~_{QG} I))$
68		elqsi	$⊢ X \in (B / (R ~_{QG} I)) \to \exists p \in B X = [p] (R ~_{QG} I)$
69	67 68	syl	$⊢ φ \to \exists p \in B X = [p] (R ~_{QG} I)$
70	65 69	r19.29a	$⊢ φ \to Y \cdot_{Q} X = X \cdot_{(O /_{𝑠} (O ~_{QG} I))} Y$
71	12 70	eqtrid	$⊢ φ \to X \cdot_{{opp}_{r} (Q)} Y = X \cdot_{(O /_{𝑠} (O ~_{QG} I))} Y$

Metamath Proof Explorer

Theorem opprqusmulr

Proof