opprqusdrng

Description: The quotient of the opposite ring is a division ring iff the opposite of the quotient ring is. (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)$
	opprqus1r.r	$⊢ φ \to R \in Ring$
	opprqus1r.i	$⊢ φ \to I \in 2Ideal (R)$
Assertion	opprqusdrng	$⊢ φ \to ({opp}_{r} (Q) \in DivRing \leftrightarrow O /_{𝑠} (O ~_{QG} I) \in DivRing)$

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	$⊢ {opp}_{r} (Q) = {opp}_{r} (Q)$
7		eqid	$⊢ 1_{Q} = 1_{Q}$
8	6 7	oppr1	$⊢ 1_{Q} = 1_{{opp}_{r} (Q)}$
9	1 2 3 4 5	opprqus1r	$⊢ φ \to 1_{{opp}_{r} (Q)} = 1_{(O /_{𝑠} (O ~_{QG} I))}$
10	8 9	eqtrid	$⊢ φ \to 1_{Q} = 1_{(O /_{𝑠} (O ~_{QG} I))}$
11		eqid	$⊢ 0_{Q} = 0_{Q}$
12	6 11	oppr0	$⊢ 0_{Q} = 0_{{opp}_{r} (Q)}$
13	5	2idllidld	$⊢ φ \to I \in LIdeal (R)$
14		lidlnsg	$⊢ (R \in Ring \land I \in LIdeal (R)) \to I \in NrmSGrp (R)$
15	4 13 14	syl2anc	$⊢ φ \to I \in NrmSGrp (R)$
16	1 2 3 15	opprqus0g	$⊢ φ \to 0_{{opp}_{r} (Q)} = 0_{(O /_{𝑠} (O ~_{QG} I))}$
17	12 16	eqtrid	$⊢ φ \to 0_{Q} = 0_{(O /_{𝑠} (O ~_{QG} I))}$
18	10 17	neeq12d	$⊢ φ \to (1_{Q} \neq 0_{Q} \leftrightarrow 1_{(O /_{𝑠} (O ~_{QG} I))} \neq 0_{(O /_{𝑠} (O ~_{QG} I))})$
19		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
20	6 19	opprbas	$⊢ {Base}_{Q} = {Base}_{{opp}_{r} (Q)}$
21		eqid	$⊢ LIdeal (R) = LIdeal (R)$
22	1 21	lidlss	$⊢ I \in LIdeal (R) \to I \subseteq B$
23	13 22	syl	$⊢ φ \to I \subseteq B$
24	1 2 3 4 23	opprqusbas	$⊢ φ \to {Base}_{{opp}_{r} (Q)} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
25	20 24	eqtrid	$⊢ φ \to {Base}_{Q} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
26	17	sneqd	$⊢ φ \to \{0_{Q}\} = \{0_{(O /_{𝑠} (O ~_{QG} I))}\}$
27	25 26	difeq12d	$⊢ φ \to {Base}_{Q} ∖ \{0_{Q}\} = {Base}_{(O /_{𝑠} (O ~_{QG} I))} ∖ \{0_{(O /_{𝑠} (O ~_{QG} I))}\}$
28	25	adantr	$⊢ (φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \to {Base}_{Q} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
29	4	ad2antrr	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to R \in Ring$
30	5	ad2antrr	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to I \in 2Ideal (R)$
31		simplr	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to x \in ({Base}_{Q} ∖ \{0_{Q}\})$
32	31	eldifad	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to x \in {Base}_{Q}$
33		simpr	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to y \in {Base}_{Q}$
34	1 2 3 29 30 19 32 33	opprqusmulr	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to x \cdot_{{opp}_{r} (Q)} y = x \cdot_{(O /_{𝑠} (O ~_{QG} I))} y$
35	10	ad2antrr	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to 1_{Q} = 1_{(O /_{𝑠} (O ~_{QG} I))}$
36	34 35	eqeq12d	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to (x \cdot_{{opp}_{r} (Q)} y = 1_{Q} \leftrightarrow x \cdot_{(O /_{𝑠} (O ~_{QG} I))} y = 1_{(O /_{𝑠} (O ~_{QG} I))})$
37	1 2 3 29 30 19 33 32	opprqusmulr	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to y \cdot_{{opp}_{r} (Q)} x = y \cdot_{(O /_{𝑠} (O ~_{QG} I))} x$
38	37 35	eqeq12d	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to (y \cdot_{{opp}_{r} (Q)} x = 1_{Q} \leftrightarrow y \cdot_{(O /_{𝑠} (O ~_{QG} I))} x = 1_{(O /_{𝑠} (O ~_{QG} I))})$
39	36 38	anbi12d	$⊢ ((φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \land y \in {Base}_{Q}) \to ((x \cdot_{{opp}_{r} (Q)} y = 1_{Q} \land y \cdot_{{opp}_{r} (Q)} x = 1_{Q}) \leftrightarrow (x \cdot_{(O /_{𝑠} (O ~_{QG} I))} y = 1_{(O /_{𝑠} (O ~_{QG} I))} \land y \cdot_{(O /_{𝑠} (O ~_{QG} I))} x = 1_{(O /_{𝑠} (O ~_{QG} I))}))$
40	28 39	rexeqbidva	$⊢ (φ \land x \in ({Base}_{Q} ∖ \{0_{Q}\})) \to (\exists y \in {Base}_{Q} (x \cdot_{{opp}_{r} (Q)} y = 1_{Q} \land y \cdot_{{opp}_{r} (Q)} x = 1_{Q}) \leftrightarrow \exists y \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (x \cdot_{(O /_{𝑠} (O ~_{QG} I))} y = 1_{(O /_{𝑠} (O ~_{QG} I))} \land y \cdot_{(O /_{𝑠} (O ~_{QG} I))} x = 1_{(O /_{𝑠} (O ~_{QG} I))}))$
41	27 40	raleqbidva	$⊢ φ \to (\forall x \in ({Base}_{Q} ∖ \{0_{Q}\}) \exists y \in {Base}_{Q} (x \cdot_{{opp}_{r} (Q)} y = 1_{Q} \land y \cdot_{{opp}_{r} (Q)} x = 1_{Q}) \leftrightarrow \forall x \in ({Base}_{(O /_{𝑠} (O ~_{QG} I))} ∖ \{0_{(O /_{𝑠} (O ~_{QG} I))}\}) \exists y \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (x \cdot_{(O /_{𝑠} (O ~_{QG} I))} y = 1_{(O /_{𝑠} (O ~_{QG} I))} \land y \cdot_{(O /_{𝑠} (O ~_{QG} I))} x = 1_{(O /_{𝑠} (O ~_{QG} I))}))$
42	18 41	anbi12d	$⊢ φ \to ((1_{Q} \neq 0_{Q} \land \forall x \in ({Base}_{Q} ∖ \{0_{Q}\}) \exists y \in {Base}_{Q} (x \cdot_{{opp}_{r} (Q)} y = 1_{Q} \land y \cdot_{{opp}_{r} (Q)} x = 1_{Q})) \leftrightarrow (1_{(O /_{𝑠} (O ~_{QG} I))} \neq 0_{(O /_{𝑠} (O ~_{QG} I))} \land \forall x \in ({Base}_{(O /_{𝑠} (O ~_{QG} I))} ∖ \{0_{(O /_{𝑠} (O ~_{QG} I))}\}) \exists y \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (x \cdot_{(O /_{𝑠} (O ~_{QG} I))} y = 1_{(O /_{𝑠} (O ~_{QG} I))} \land y \cdot_{(O /_{𝑠} (O ~_{QG} I))} x = 1_{(O /_{𝑠} (O ~_{QG} I))})))$
43		eqid	$⊢ \cdot_{{opp}_{r} (Q)} = \cdot_{{opp}_{r} (Q)}$
44		eqid	$⊢ Unit (Q) = Unit (Q)$
45	44 6	opprunit	$⊢ Unit (Q) = Unit ({opp}_{r} (Q))$
46		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
47	3 46	qusring	$⊢ (R \in Ring \land I \in 2Ideal (R)) \to Q \in Ring$
48	4 5 47	syl2anc	$⊢ φ \to Q \in Ring$
49	6	opprring	$⊢ Q \in Ring \to {opp}_{r} (Q) \in Ring$
50	48 49	syl	$⊢ φ \to {opp}_{r} (Q) \in Ring$
51	20 12 8 43 45 50	isdrng4	$⊢ φ \to ({opp}_{r} (Q) \in DivRing \leftrightarrow (1_{Q} \neq 0_{Q} \land \forall x \in ({Base}_{Q} ∖ \{0_{Q}\}) \exists y \in {Base}_{Q} (x \cdot_{{opp}_{r} (Q)} y = 1_{Q} \land y \cdot_{{opp}_{r} (Q)} x = 1_{Q})))$
52		eqid	$⊢ {Base}_{(O /_{𝑠} (O ~_{QG} I))} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
53		eqid	$⊢ 0_{(O /_{𝑠} (O ~_{QG} I))} = 0_{(O /_{𝑠} (O ~_{QG} I))}$
54		eqid	$⊢ 1_{(O /_{𝑠} (O ~_{QG} I))} = 1_{(O /_{𝑠} (O ~_{QG} I))}$
55		eqid	$⊢ \cdot_{(O /_{𝑠} (O ~_{QG} I))} = \cdot_{(O /_{𝑠} (O ~_{QG} I))}$
56		eqid	$⊢ Unit (O /_{𝑠} (O ~_{QG} I)) = Unit (O /_{𝑠} (O ~_{QG} I))$
57	2	opprring	$⊢ R \in Ring \to O \in Ring$
58	4 57	syl	$⊢ φ \to O \in Ring$
59	2 4	oppr2idl	$⊢ φ \to 2Ideal (R) = 2Ideal (O)$
60	5 59	eleqtrd	$⊢ φ \to I \in 2Ideal (O)$
61		eqid	$⊢ O /_{𝑠} (O ~_{QG} I) = O /_{𝑠} (O ~_{QG} I)$
62		eqid	$⊢ 2Ideal (O) = 2Ideal (O)$
63	61 62	qusring	$⊢ (O \in Ring \land I \in 2Ideal (O)) \to O /_{𝑠} (O ~_{QG} I) \in Ring$
64	58 60 63	syl2anc	$⊢ φ \to O /_{𝑠} (O ~_{QG} I) \in Ring$
65	52 53 54 55 56 64	isdrng4	$⊢ φ \to (O /_{𝑠} (O ~_{QG} I) \in DivRing \leftrightarrow (1_{(O /_{𝑠} (O ~_{QG} I))} \neq 0_{(O /_{𝑠} (O ~_{QG} I))} \land \forall x \in ({Base}_{(O /_{𝑠} (O ~_{QG} I))} ∖ \{0_{(O /_{𝑠} (O ~_{QG} I))}\}) \exists y \in {Base}_{(O /_{𝑠} (O ~_{QG} I))} (x \cdot_{(O /_{𝑠} (O ~_{QG} I))} y = 1_{(O /_{𝑠} (O ~_{QG} I))} \land y \cdot_{(O /_{𝑠} (O ~_{QG} I))} x = 1_{(O /_{𝑠} (O ~_{QG} I))})))$
66	42 51 65	3bitr4d	$⊢ φ \to ({opp}_{r} (Q) \in DivRing \leftrightarrow O /_{𝑠} (O ~_{QG} I) \in DivRing)$

Metamath Proof Explorer

Theorem opprqusdrng

Proof