Theorem 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={\mathrm{Base}}_R$$
	opprqus.o	$$⊢O={opp}_r\left(R\right)$$
	opprqus.q	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
	opprqus.i	$$⊢\phi \to I\in \mathrm{NrmSGrp}\left(R\right)$$
Assertion	opprqus0g	$$⊢\phi \to 0_{{opp}_r\left(Q\right)}=0_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}$$

Proof

Step	Hyp	Ref	Expression
1		opprqus.b	$$⊢B={\mathrm{Base}}_R$$
2		opprqus.o	$$⊢O={opp}_r\left(R\right)$$
3		opprqus.q	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
4		opprqus.i	$$⊢\phi \to I\in \mathrm{NrmSGrp}\left(R\right)$$
5	4	elfvexd	$$⊢\phi \to R\in \mathrm{V}$$
6		nsgsubg	$$⊢I\in \mathrm{NrmSGrp}\left(R\right)\to I\in \mathrm{SubGrp}\left(R\right)$$
7	1	subgss	$$⊢I\in \mathrm{SubGrp}\left(R\right)\to I\subseteq B$$
8	4 6 7	3syl	$$⊢\phi \to I\subseteq B$$
9	1 2 3 5 8	opprqusbas	$$⊢\phi \to {\mathrm{Base}}_{{opp}_r\left(Q\right)}={\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}$$
10	9	adantr	$$⊢\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to {\mathrm{Base}}_{{opp}_r\left(Q\right)}={\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}$$
11	4	ad2antrr	$$⊢\left(\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to I\in \mathrm{NrmSGrp}\left(R\right)$$
12		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
13		simpr	$$⊢\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}$$
14		eqid	$$⊢{opp}_r\left(Q\right)={opp}_r\left(Q\right)$$
15	14 12	opprbas	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_{{opp}_r\left(Q\right)}$$
16	15	eqcomi	$$⊢{\mathrm{Base}}_{{opp}_r\left(Q\right)}={\mathrm{Base}}_Q$$
17	13 16	eleqtrdi	$$⊢\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to e\in {\mathrm{Base}}_Q$$
18	17	adantr	$$⊢\left(\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to e\in {\mathrm{Base}}_Q$$
19		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}$$
20	19 16	eleqtrdi	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to x\in {\mathrm{Base}}_Q$$
21	20	adantlr	$$⊢\left(\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to x\in {\mathrm{Base}}_Q$$
22	1 2 3 11 12 18 21	opprqusplusg	$$⊢\left(\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to e{+}_{{opp}_r\left(Q\right)}x=e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x$$
23	22	eqeq1d	$$⊢\left(\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to \left(e{+}_{{opp}_r\left(Q\right)}x=x\leftrightarrow e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x=x\right)$$
24	1 2 3 11 12 21 18	opprqusplusg	$$⊢\left(\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to x{+}_{{opp}_r\left(Q\right)}e=x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e$$
25	24	eqeq1d	$$⊢\left(\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to \left(x{+}_{{opp}_r\left(Q\right)}e=x\leftrightarrow x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e=x\right)$$
26	23 25	anbi12d	$$⊢\left(\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\wedge x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to \left(\left(e{+}_{{opp}_r\left(Q\right)}x=x\wedge x{+}_{{opp}_r\left(Q\right)}e=x\right)\leftrightarrow \left(e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x=x\wedge x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e=x\right)\right)$$
27	10 26	raleqbidva	$$⊢\left(\phi \wedge e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\right)\to \left(\forall x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\left(e{+}_{{opp}_r\left(Q\right)}x=x\wedge x{+}_{{opp}_r\left(Q\right)}e=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\left(e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x=x\wedge x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e=x\right)\right)$$
28	27	pm5.32da	$$⊢\phi \to \left(\left(e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\wedge \forall x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\left(e{+}_{{opp}_r\left(Q\right)}x=x\wedge x{+}_{{opp}_r\left(Q\right)}e=x\right)\right)\leftrightarrow \left(e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\wedge \forall x\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\left(e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x=x\wedge x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e=x\right)\right)\right)$$
29	9	eleq2d	$$⊢\phi \to \left(e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\leftrightarrow e\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\right)$$
30	29	anbi1d	$$⊢\phi \to \left(\left(e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\wedge \forall x\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\left(e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x=x\wedge x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e=x\right)\right)\leftrightarrow \left(e\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\wedge \forall x\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\left(e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x=x\wedge x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e=x\right)\right)\right)$$
31	28 30	bitrd	$$⊢\phi \to \left(\left(e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\wedge \forall x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\left(e{+}_{{opp}_r\left(Q\right)}x=x\wedge x{+}_{{opp}_r\left(Q\right)}e=x\right)\right)\leftrightarrow \left(e\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\wedge \forall x\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\left(e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x=x\wedge x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e=x\right)\right)\right)$$
32	31	iotabidv	$$⊢\phi \to \left(\iota e|\left(e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\wedge \forall x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\left(e{+}_{{opp}_r\left(Q\right)}x=x\wedge x{+}_{{opp}_r\left(Q\right)}e=x\right)\right)\right)=\left(\iota e|\left(e\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\wedge \forall x\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\left(e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x=x\wedge x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e=x\right)\right)\right)$$
33		eqid	$$⊢{+}_Q={+}_Q$$
34	14 33	oppradd	$$⊢{+}_Q={+}_{{opp}_r\left(Q\right)}$$
35	34	eqcomi	$$⊢{+}_{{opp}_r\left(Q\right)}={+}_Q$$
36		eqid	$$⊢0_Q=0_Q$$
37	14 36	oppr0	$$⊢0_Q=0_{{opp}_r\left(Q\right)}$$
38	37	eqcomi	$$⊢0_{{opp}_r\left(Q\right)}=0_Q$$
39	16 35 38	grpidval	$$⊢0_{{opp}_r\left(Q\right)}=\left(\iota e|\left(e\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\wedge \forall x\in {\mathrm{Base}}_{{opp}_r\left(Q\right)}\left(e{+}_{{opp}_r\left(Q\right)}x=x\wedge x{+}_{{opp}_r\left(Q\right)}e=x\right)\right)\right)$$
40		eqid	$$⊢{\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}={\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}$$
41		eqid	$$⊢{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}={+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}$$
42		eqid	$$⊢0_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}=0_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}$$
43	40 41 42	grpidval	$$⊢0_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}=\left(\iota e|\left(e\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\wedge \forall x\in {\mathrm{Base}}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}\left(e{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}x=x\wedge x{+}_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}e=x\right)\right)\right)$$
44	32 39 43	3eqtr4g	$$⊢\phi \to 0_{{opp}_r\left(Q\right)}=0_{\left(O{/}_{𝑠}\left(O{~}_{\mathit{QG}}I\right)\right)}$$