Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
opprqus.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
opprqus.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
opprqus1r.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
opprqus1r.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
Assertion opprqusdrng ( 𝜑 → ( ( oppr ‘ 𝑄 ) ∈ DivRing ↔ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ∈ DivRing ) )

Proof

Step Hyp Ref Expression
1 opprqus.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 opprqus.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
3 opprqus.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
4 opprqus1r.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 opprqus1r.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
6 eqid ⊢ ( oppr ‘ 𝑄 ) = ( oppr ‘ 𝑄 )
7 eqid ⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ 𝑄 )
8 6 7 oppr1 ⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ ( oppr ‘ 𝑄 ) )
9 1 2 3 4 5 opprqus1r ⊢ ( 𝜑 → ( 1r ‘ ( oppr ‘ 𝑄 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
10 8 9 eqtrid ⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
11 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
12 6 11 oppr0 ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ ( oppr ‘ 𝑄 ) )
13 5 2idllidld ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
14 lidlnsg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
15 4 13 14 syl2anc ⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
16 1 2 3 15 opprqus0g ⊢ ( 𝜑 → ( 0g ‘ ( oppr ‘ 𝑄 ) ) = ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
17 12 16 eqtrid ⊢ ( 𝜑 → ( 0g ‘ 𝑄 ) = ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
18 10 17 neeq12d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑄 ) ≠ ( 0g ‘ 𝑄 ) ↔ ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ≠ ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ) )
19 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
20 6 19 opprbas ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( oppr ‘ 𝑄 ) )
21 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
22 1 21 lidlss ⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
23 13 22 syl ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
24 1 2 3 4 23 opprqusbas ⊢ ( 𝜑 → ( Base ‘ ( oppr ‘ 𝑄 ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
25 20 24 eqtrid ⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
26 17 sneqd ⊢ ( 𝜑 → { ( 0g ‘ 𝑄 ) } = { ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) } )
27 25 26 difeq12d ⊢ ( 𝜑 → ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) = ( ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∖ { ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) } ) )
28 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) → ( Base ‘ 𝑄 ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
29 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → 𝑅 ∈ Ring )
30 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) )
32 31 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → 𝑥 ∈ ( Base ‘ 𝑄 ) )
33 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → 𝑦 ∈ ( Base ‘ 𝑄 ) )
34 1 2 3 29 30 19 32 33 opprqusmulr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑦 ) )
35 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → ( 1r ‘ 𝑄 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
36 34 35 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑦 ) = ( 1r ‘ 𝑄 ) ↔ ( 𝑥 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ) )
37 1 2 3 29 30 19 33 32 opprqusmulr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑥 ) = ( 𝑦 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) )
38 37 35 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → ( ( 𝑦 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑥 ) = ( 1r ‘ 𝑄 ) ↔ ( 𝑦 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ) )
39 36 38 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) → ( ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑦 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑥 ) = ( 1r ‘ 𝑄 ) ) ↔ ( ( 𝑥 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ) ) )
40 28 39 rexeqbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) → ( ∃ 𝑦 ∈ ( Base ‘ 𝑄 ) ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑦 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑥 ) = ( 1r ‘ 𝑄 ) ) ↔ ∃ 𝑦 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑥 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ) ) )
41 27 40 raleqbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ∃ 𝑦 ∈ ( Base ‘ 𝑄 ) ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑦 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑥 ) = ( 1r ‘ 𝑄 ) ) ↔ ∀ 𝑥 ∈ ( ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∖ { ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) } ) ∃ 𝑦 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑥 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ) ) )
42 18 41 anbi12d ⊢ ( 𝜑 → ( ( ( 1r ‘ 𝑄 ) ≠ ( 0g ‘ 𝑄 ) ∧ ∀ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ∃ 𝑦 ∈ ( Base ‘ 𝑄 ) ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑦 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑥 ) = ( 1r ‘ 𝑄 ) ) ) ↔ ( ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ≠ ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ∀ 𝑥 ∈ ( ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∖ { ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) } ) ∃ 𝑦 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑥 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ) ) ) )
43 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑄 ) ) = ( .r ‘ ( oppr ‘ 𝑄 ) )
44 eqid ⊢ ( Unit ‘ 𝑄 ) = ( Unit ‘ 𝑄 )
45 44 6 opprunit ⊢ ( Unit ‘ 𝑄 ) = ( Unit ‘ ( oppr ‘ 𝑄 ) )
46 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
47 3 46 qusring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) → 𝑄 ∈ Ring )
48 4 5 47 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ Ring )
49 6 opprring ⊢ ( 𝑄 ∈ Ring → ( oppr ‘ 𝑄 ) ∈ Ring )
50 48 49 syl ⊢ ( 𝜑 → ( oppr ‘ 𝑄 ) ∈ Ring )
51 20 12 8 43 45 50 isdrng4 ⊢ ( 𝜑 → ( ( oppr ‘ 𝑄 ) ∈ DivRing ↔ ( ( 1r ‘ 𝑄 ) ≠ ( 0g ‘ 𝑄 ) ∧ ∀ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ∃ 𝑦 ∈ ( Base ‘ 𝑄 ) ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑦 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑥 ) = ( 1r ‘ 𝑄 ) ) ) ) )
52 eqid ⊢ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
53 eqid ⊢ ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
54 eqid ⊢ ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
55 eqid ⊢ ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
56 eqid ⊢ ( Unit ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( Unit ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
57 2 opprring ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )
58 4 57 syl ⊢ ( 𝜑 → 𝑂 ∈ Ring )
59 2 4 oppr2idl ⊢ ( 𝜑 → ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑂 ) )
60 5 59 eleqtrd ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑂 ) )
61 eqid ⊢ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) = ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) )
62 eqid ⊢ ( 2Ideal ‘ 𝑂 ) = ( 2Ideal ‘ 𝑂 )
63 61 62 qusring ⊢ ( ( 𝑂 ∈ Ring ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑂 ) ) → ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ∈ Ring )
64 58 60 63 syl2anc ⊢ ( 𝜑 → ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ∈ Ring )
65 52 53 54 55 56 64 isdrng4 ⊢ ( 𝜑 → ( ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ∈ DivRing ↔ ( ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ≠ ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ∀ 𝑥 ∈ ( ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∖ { ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) } ) ∃ 𝑦 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑥 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ) ) ) )
66 42 51 65 3bitr4d ⊢ ( 𝜑 → ( ( oppr ‘ 𝑄 ) ∈ DivRing ↔ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ∈ DivRing ) )