opprqusplusg

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

	Ref	Expression
Hypotheses	opprqus.b	$⊢ B = {Base}_{R}$
	opprqus.o	$⊢ O = {opp}_{r} (R)$
	opprqus.q	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
	opprqus.i	$⊢ φ \to I \in NrmSGrp (R)$
	opprqusplusg.e	$⊢ E = {Base}_{Q}$
	opprqusplusg.x	$⊢ φ \to X \in E$
	opprqusplusg.y	$⊢ φ \to Y \in E$
Assertion	opprqusplusg	$⊢ φ \to X +_{{opp}_{r} (Q)} Y = X +_{(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		opprqus.i	$⊢ φ \to I \in NrmSGrp (R)$
5		opprqusplusg.e	$⊢ E = {Base}_{Q}$
6		opprqusplusg.x	$⊢ φ \to X \in E$
7		opprqusplusg.y	$⊢ φ \to Y \in E$
8		eqid	$⊢ {opp}_{r} (Q) = {opp}_{r} (Q)$
9		eqid	$⊢ +_{Q} = +_{Q}$
10	8 9	oppradd	$⊢ +_{Q} = +_{{opp}_{r} (Q)}$
11	10	oveqi	$⊢ X +_{Q} Y = X +_{{opp}_{r} (Q)} Y$
12	4	ad4antr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to I \in NrmSGrp (R)$
13		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$
14		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$
15		eqid	$⊢ +_{R} = +_{R}$
16	3 1 15 9	qusadd	$⊢ (I \in NrmSGrp (R) \land p \in B \land q \in B) \to [p] (R ~_{QG} I) +_{Q} [q] (R ~_{QG} I) = [(p +_{R} q)] (R ~_{QG} I)$
17	12 13 14 16	syl3anc	$⊢ ((((φ \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) +_{Q} [q] (R ~_{QG} I) = [(p +_{R} q)] (R ~_{QG} I)$
18		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)$
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	18 19	oveq12d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to X +_{Q} Y = [p] (R ~_{QG} I) +_{Q} [q] (R ~_{QG} I)$
21	4	elfvexd	$⊢ φ \to R \in V$
22		nsgsubg	$⊢ I \in NrmSGrp (R) \to I \in SubGrp (R)$
23	1	subgss	$⊢ I \in SubGrp (R) \to I \subseteq B$
24	4 22 23	3syl	$⊢ φ \to I \subseteq B$
25	2 1	oppreqg	$⊢ (R \in V \land I \subseteq B) \to R ~_{QG} I = O ~_{QG} I$
26	21 24 25	syl2anc	$⊢ φ \to R ~_{QG} I = O ~_{QG} I$
27	26	eceq2d	$⊢ φ \to [p] (R ~_{QG} I) = [p] (O ~_{QG} I)$
28	26	eceq2d	$⊢ φ \to [q] (R ~_{QG} I) = [q] (O ~_{QG} I)$
29	27 28	oveq12d	$⊢ φ \to [p] (R ~_{QG} I) +_{(O /_{𝑠} (O ~_{QG} I))} [q] (R ~_{QG} I) = [p] (O ~_{QG} I) +_{(O /_{𝑠} (O ~_{QG} I))} [q] (O ~_{QG} I)$
30	29	ad4antr	$⊢ ((((φ \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) +_{(O /_{𝑠} (O ~_{QG} I))} [q] (R ~_{QG} I) = [p] (O ~_{QG} I) +_{(O /_{𝑠} (O ~_{QG} I))} [q] (O ~_{QG} I)$
31	2	opprnsg	$⊢ NrmSGrp (R) = NrmSGrp (O)$
32	4 31	eleqtrdi	$⊢ φ \to I \in NrmSGrp (O)$
33	32	ad4antr	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to I \in NrmSGrp (O)$
34	13 1	eleqtrdi	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to p \in {Base}_{R}$
35	14 1	eleqtrdi	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to q \in {Base}_{R}$
36		eqid	$⊢ O /_{𝑠} (O ~_{QG} I) = O /_{𝑠} (O ~_{QG} I)$
37	2 1	opprbas	$⊢ B = {Base}_{O}$
38	1 37	eqtr3i	$⊢ {Base}_{R} = {Base}_{O}$
39	2 15	oppradd	$⊢ +_{R} = +_{O}$
40		eqid	$⊢ +_{(O /_{𝑠} (O ~_{QG} I))} = +_{(O /_{𝑠} (O ~_{QG} I))}$
41	36 38 39 40	qusadd	$⊢ (I \in NrmSGrp (O) \land p \in {Base}_{R} \land q \in {Base}_{R}) \to [p] (O ~_{QG} I) +_{(O /_{𝑠} (O ~_{QG} I))} [q] (O ~_{QG} I) = [(p +_{R} q)] (O ~_{QG} I)$
42	33 34 35 41	syl3anc	$⊢ ((((φ \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) +_{(O /_{𝑠} (O ~_{QG} I))} [q] (O ~_{QG} I) = [(p +_{R} q)] (O ~_{QG} I)$
43	30 42	eqtrd	$⊢ ((((φ \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) +_{(O /_{𝑠} (O ~_{QG} I))} [q] (R ~_{QG} I) = [(p +_{R} q)] (O ~_{QG} I)$
44	18 19	oveq12d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to X +_{(O /_{𝑠} (O ~_{QG} I))} Y = [p] (R ~_{QG} I) +_{(O /_{𝑠} (O ~_{QG} I))} [q] (R ~_{QG} I)$
45	26	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$
46	45	eceq2d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to [(p +_{R} q)] (R ~_{QG} I) = [(p +_{R} q)] (O ~_{QG} I)$
47	43 44 46	3eqtr4d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to X +_{(O /_{𝑠} (O ~_{QG} I))} Y = [(p +_{R} q)] (R ~_{QG} I)$
48	17 20 47	3eqtr4d	$⊢ ((((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \land q \in B) \land Y = [q] (R ~_{QG} I)) \to X +_{Q} Y = X +_{(O /_{𝑠} (O ~_{QG} I))} Y$
49	3	a1i	$⊢ φ \to Q = R /_{𝑠} (R ~_{QG} I)$
50	1	a1i	$⊢ φ \to B = {Base}_{R}$
51		ovexd	$⊢ φ \to R ~_{QG} I \in V$
52	49 50 51 21	qusbas	$⊢ φ \to B / (R ~_{QG} I) = {Base}_{Q}$
53	5 52	eqtr4id	$⊢ φ \to E = B / (R ~_{QG} I)$
54	7 53	eleqtrd	$⊢ φ \to Y \in (B / (R ~_{QG} I))$
55	54	ad2antrr	$⊢ ((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \to Y \in (B / (R ~_{QG} I))$
56		elqsi	$⊢ Y \in (B / (R ~_{QG} I)) \to \exists q \in B Y = [q] (R ~_{QG} I)$
57	55 56	syl	$⊢ ((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \to \exists q \in B Y = [q] (R ~_{QG} I)$
58	48 57	r19.29a	$⊢ ((φ \land p \in B) \land X = [p] (R ~_{QG} I)) \to X +_{Q} Y = X +_{(O /_{𝑠} (O ~_{QG} I))} Y$
59	6 53	eleqtrd	$⊢ φ \to X \in (B / (R ~_{QG} I))$
60		elqsi	$⊢ X \in (B / (R ~_{QG} I)) \to \exists p \in B X = [p] (R ~_{QG} I)$
61	59 60	syl	$⊢ φ \to \exists p \in B X = [p] (R ~_{QG} I)$
62	58 61	r19.29a	$⊢ φ \to X +_{Q} Y = X +_{(O /_{𝑠} (O ~_{QG} I))} Y$
63	11 62	eqtr3id	$⊢ φ \to X +_{{opp}_{r} (Q)} Y = X +_{(O /_{𝑠} (O ~_{QG} I))} Y$

Metamath Proof Explorer

Theorem opprqusplusg

Proof