opprqus0g

Description: The group identity element of the quotient of the opposite ring is the same as the group identity element 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)$
Assertion	opprqus0g	$⊢ φ \to 0_{{opp}_{r} (Q)} = 0_{(O /_{𝑠} (O ~_{QG} I))}$

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	4	elfvexd	$⊢ φ \to R \in V$
6		nsgsubg	$⊢ I \in NrmSGrp (R) \to I \in SubGrp (R)$
7	1	subgss	$⊢ I \in SubGrp (R) \to I \subseteq B$
8	4 6 7	3syl	$⊢ φ \to I \subseteq B$
9	1 2 3 5 8	opprqusbas	$⊢ φ \to {Base}_{{opp}_{r} (Q)} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
10	9	adantr	$⊢ (φ \land e \in {Base}_{{opp}_{r} (Q)}) \to {Base}_{{opp}_{r} (Q)} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
11	4	ad2antrr	$⊢ ((φ \land e \in {Base}_{{opp}_{r} (Q)}) \land x \in {Base}_{{opp}_{r} (Q)}) \to I \in NrmSGrp (R)$
12		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
13		simpr	$⊢ (φ \land e \in {Base}_{{opp}_{r} (Q)}) \to e \in {Base}_{{opp}_{r} (Q)}$
14		eqid	$⊢ {opp}_{r} (Q) = {opp}_{r} (Q)$
15	14 12	opprbas	$⊢ {Base}_{Q} = {Base}_{{opp}_{r} (Q)}$
16	15	eqcomi	$⊢ {Base}_{{opp}_{r} (Q)} = {Base}_{Q}$
17	13 16	eleqtrdi	$⊢ (φ \land e \in {Base}_{{opp}_{r} (Q)}) \to e \in {Base}_{Q}$
18	17	adantr	$⊢ ((φ \land e \in {Base}_{{opp}_{r} (Q)}) \land x \in {Base}_{{opp}_{r} (Q)}) \to e \in {Base}_{Q}$
19		simpr	$⊢ (φ \land x \in {Base}_{{opp}_{r} (Q)}) \to x \in {Base}_{{opp}_{r} (Q)}$
20	19 16	eleqtrdi	$⊢ (φ \land x \in {Base}_{{opp}_{r} (Q)}) \to x \in {Base}_{Q}$
21	20	adantlr	$⊢ ((φ \land e \in {Base}_{{opp}_{r} (Q)}) \land x \in {Base}_{{opp}_{r} (Q)}) \to x \in {Base}_{Q}$
22	1 2 3 11 12 18 21	opprqusplusg	$⊢ ((φ \land e \in {Base}_{{opp}_{r} (Q)}) \land x \in {Base}_{{opp}_{r} (Q)}) \to e +_{{opp}_{r} (Q)} x = e +_{(O /_{𝑠} (O ~_{QG} I))} x$
23	22	eqeq1d	$⊢ ((φ \land e \in {Base}_{{opp}_{r} (Q)}) \land x \in {Base}_{{opp}_{r} (Q)}) \to (e +_{{opp}_{r} (Q)} x = x \leftrightarrow e +_{(O /_{𝑠} (O ~_{QG} I))} x = x)$
24	1 2 3 11 12 21 18	opprqusplusg	$⊢ ((φ \land e \in {Base}_{{opp}_{r} (Q)}) \land x \in {Base}_{{opp}_{r} (Q)}) \to x +_{{opp}_{r} (Q)} e = x +_{(O /_{𝑠} (O ~_{QG} I))} e$
25	24	eqeq1d	$⊢ ((φ \land e \in {Base}_{{opp}_{r} (Q)}) \land x \in {Base}_{{opp}_{r} (Q)}) \to (x +_{{opp}_{r} (Q)} e = x \leftrightarrow x +_{(O /_{𝑠} (O ~_{QG} I))} e = x)$
26	23 25	anbi12d	$⊢ ((φ \land e \in {Base}_{{opp}_{r} (Q)}) \land x \in {Base}_{{opp}_{r} (Q)}) \to ((e +_{{opp}_{r} (Q)} x = x \land x +_{{opp}_{r} (Q)} e = x) \leftrightarrow (e +_{(O /_{𝑠} (O ~_{QG} I))} x = x \land x +_{(O /_{𝑠} (O ~_{QG} I))} e = x))$
27	10 26	raleqbidva	$⊢ (φ \land e \in {Base}_{{opp}_{r} (Q)}) \to (\forall x \in {Base}_{{opp}_{r} (Q)} (e +_{{opp}_{r} (Q)} x = x \land x +_{{opp}_{r} (Q)} e = x) \leftrightarrow \forall x \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (e +_{(O /_{𝑠} (O ~_{QG} I))} x = x \land x +_{(O /_{𝑠} (O ~_{QG} I))} e = x))$
28	27	pm5.32da	$⊢ φ \to ((e \in {Base}_{{opp}_{r} (Q)} \land \forall x \in {Base}_{{opp}_{r} (Q)} (e +_{{opp}_{r} (Q)} x = x \land x +_{{opp}_{r} (Q)} e = x)) \leftrightarrow (e \in {Base}_{{opp}_{r} (Q)} \land \forall x \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (e +_{(O /_{𝑠} (O ~_{QG} I))} x = x \land x +_{(O /_{𝑠} (O ~_{QG} I))} e = x)))$
29	9	eleq2d	$⊢ φ \to (e \in {Base}_{{opp}_{r} (Q)} \leftrightarrow e \in {Base}_{(O /_{𝑠} (O ~_{QG} I))})$
30	29	anbi1d	$⊢ φ \to ((e \in {Base}_{{opp}_{r} (Q)} \land \forall x \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (e +_{(O /_{𝑠} (O ~_{QG} I))} x = x \land x +_{(O /_{𝑠} (O ~_{QG} I))} e = x)) \leftrightarrow (e \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} \land \forall x \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (e +_{(O /_{𝑠} (O ~_{QG} I))} x = x \land x +_{(O /_{𝑠} (O ~_{QG} I))} e = x)))$
31	28 30	bitrd	$⊢ φ \to ((e \in {Base}_{{opp}_{r} (Q)} \land \forall x \in {Base}_{{opp}_{r} (Q)} (e +_{{opp}_{r} (Q)} x = x \land x +_{{opp}_{r} (Q)} e = x)) \leftrightarrow (e \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} \land \forall x \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (e +_{(O /_{𝑠} (O ~_{QG} I))} x = x \land x +_{(O /_{𝑠} (O ~_{QG} I))} e = x)))$
32	31	iotabidv	$⊢ φ \to (ι e \| (e \in {Base}_{{opp}_{r} (Q)} \land \forall x \in {Base}_{{opp}_{r} (Q)} (e +_{{opp}_{r} (Q)} x = x \land x +_{{opp}_{r} (Q)} e = x))) = (ι e \| (e \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} \land \forall x \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (e +_{(O /_{𝑠} (O ~_{QG} I))} x = x \land x +_{(O /_{𝑠} (O ~_{QG} I))} e = x)))$
33		eqid	$⊢ +_{Q} = +_{Q}$
34	14 33	oppradd	$⊢ +_{Q} = +_{{opp}_{r} (Q)}$
35	34	eqcomi	$⊢ +_{{opp}_{r} (Q)} = +_{Q}$
36		eqid	$⊢ 0_{Q} = 0_{Q}$
37	14 36	oppr0	$⊢ 0_{Q} = 0_{{opp}_{r} (Q)}$
38	37	eqcomi	$⊢ 0_{{opp}_{r} (Q)} = 0_{Q}$
39	16 35 38	grpidval	$⊢ 0_{{opp}_{r} (Q)} = (ι e \| (e \in {Base}_{{opp}_{r} (Q)} \land \forall x \in {Base}_{{opp}_{r} (Q)} (e +_{{opp}_{r} (Q)} x = x \land x +_{{opp}_{r} (Q)} e = x)))$
40		eqid	$⊢ {Base}_{(O /_{𝑠} (O ~_{QG} I))} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
41		eqid	$⊢ +_{(O /_{𝑠} (O ~_{QG} I))} = +_{(O /_{𝑠} (O ~_{QG} I))}$
42		eqid	$⊢ 0_{(O /_{𝑠} (O ~_{QG} I))} = 0_{(O /_{𝑠} (O ~_{QG} I))}$
43	40 41 42	grpidval	$⊢ 0_{(O /_{𝑠} (O ~_{QG} I))} = (ι e \| (e \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} \land \forall x \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (e +_{(O /_{𝑠} (O ~_{QG} I))} x = x \land x +_{(O /_{𝑠} (O ~_{QG} I))} e = x)))$
44	32 39 43	3eqtr4g	$⊢ φ \to 0_{{opp}_{r} (Q)} = 0_{(O /_{𝑠} (O ~_{QG} I))}$

Metamath Proof Explorer

Theorem opprqus0g

Proof