opprqus1r

Description: The ring unity of the quotient of the opposite ring is the same as the ring unity 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)$
Assertion	opprqus1r	$⊢ φ \to 1_{{opp}_{r} (Q)} = 1_{(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		opprqus1r.r	$⊢ φ \to R \in Ring$
5		opprqus1r.i	$⊢ φ \to I \in 2Ideal (R)$
6		eqid	$⊢ {Base}_{{opp}_{r} (Q)} = {Base}_{{opp}_{r} (Q)}$
7		fvexd	$⊢ φ \to {opp}_{r} (Q) \in V$
8		ovexd	$⊢ φ \to O /_{𝑠} (O ~_{QG} I) \in V$
9	5	2idllidld	$⊢ φ \to I \in LIdeal (R)$
10		eqid	$⊢ LIdeal (R) = LIdeal (R)$
11	1 10	lidlss	$⊢ I \in LIdeal (R) \to I \subseteq B$
12	9 11	syl	$⊢ φ \to I \subseteq B$
13	1 2 3 4 12	opprqusbas	$⊢ φ \to {Base}_{{opp}_{r} (Q)} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
14	4	ad2antrr	$⊢ ((φ \land x \in {Base}_{{opp}_{r} (Q)}) \land y \in {Base}_{{opp}_{r} (Q)}) \to R \in Ring$
15	5	ad2antrr	$⊢ ((φ \land x \in {Base}_{{opp}_{r} (Q)}) \land y \in {Base}_{{opp}_{r} (Q)}) \to I \in 2Ideal (R)$
16		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
17		simpr	$⊢ (φ \land x \in {Base}_{{opp}_{r} (Q)}) \to x \in {Base}_{{opp}_{r} (Q)}$
18		eqid	$⊢ {opp}_{r} (Q) = {opp}_{r} (Q)$
19	18 16	opprbas	$⊢ {Base}_{Q} = {Base}_{{opp}_{r} (Q)}$
20	17 19	eleqtrrdi	$⊢ (φ \land x \in {Base}_{{opp}_{r} (Q)}) \to x \in {Base}_{Q}$
21	20	adantr	$⊢ ((φ \land x \in {Base}_{{opp}_{r} (Q)}) \land y \in {Base}_{{opp}_{r} (Q)}) \to x \in {Base}_{Q}$
22		simpr	$⊢ (φ \land y \in {Base}_{{opp}_{r} (Q)}) \to y \in {Base}_{{opp}_{r} (Q)}$
23	22 19	eleqtrrdi	$⊢ (φ \land y \in {Base}_{{opp}_{r} (Q)}) \to y \in {Base}_{Q}$
24	23	adantlr	$⊢ ((φ \land x \in {Base}_{{opp}_{r} (Q)}) \land y \in {Base}_{{opp}_{r} (Q)}) \to y \in {Base}_{Q}$
25	1 2 3 14 15 16 21 24	opprqusmulr	$⊢ ((φ \land x \in {Base}_{{opp}_{r} (Q)}) \land y \in {Base}_{{opp}_{r} (Q)}) \to x \cdot_{{opp}_{r} (Q)} y = x \cdot_{(O /_{𝑠} (O ~_{QG} I))} y$
26	6 7 8 13 25	urpropd	$⊢ φ \to 1_{{opp}_{r} (Q)} = 1_{(O /_{𝑠} (O ~_{QG} I))}$

Metamath Proof Explorer

Theorem opprqus1r

Proof