Metamath Proof Explorer

Theorem opprqusmulr

Description: The multiplication operation of the quotient of the opposite ring is the same as the multiplication operation of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses opprqus.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
opprqus.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
opprqus.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
opprqus1r.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
opprqus1r.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
opprqusmulr.e ⊢ 𝐸 = ( Base ‘ 𝑄 )
opprqusmulr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
opprqusmulr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
Assertion opprqusmulr ( 𝜑 → ( 𝑋 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑌 ) = ( 𝑋 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) )

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 opprqusmulr.e ⊢ 𝐸 = ( Base ‘ 𝑄 )
7 opprqusmulr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
8 opprqusmulr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
9 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
10 eqid ⊢ ( oppr ‘ 𝑄 ) = ( oppr ‘ 𝑄 )
11 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑄 ) ) = ( .r ‘ ( oppr ‘ 𝑄 ) )
12 6 9 10 11 opprmul ⊢ ( 𝑋 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑌 ) = ( 𝑌 ( .r ‘ 𝑄 ) 𝑋 )
13 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
14 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑅 ∈ Ring )
15 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
16 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑞 ∈ 𝐵 )
17 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑝 ∈ 𝐵 )
18 3 1 13 9 14 15 16 17 qusmul2idl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑞 ( .r ‘ 𝑅 ) 𝑝 ) ] ( 𝑅 ~QG 𝐼 ) )
19 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) )
20 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) )
21 19 20 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑌 ( .r ‘ 𝑄 ) 𝑋 ) = ( [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) )
22 eqid ⊢ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) = ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) )
23 2 1 opprbas ⊢ 𝐵 = ( Base ‘ 𝑂 )
24 eqid ⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
25 eqid ⊢ ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
26 2 opprring ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )
27 4 26 syl ⊢ ( 𝜑 → 𝑂 ∈ Ring )
28 27 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑂 ∈ Ring )
29 2 4 oppr2idl ⊢ ( 𝜑 → ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑂 ) )
30 5 29 eleqtrd ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑂 ) )
31 30 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑂 ) )
32 22 23 24 25 28 31 17 16 qusmul2idl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑝 ] ( 𝑂 ~QG 𝐼 ) ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑂 ~QG 𝐼 ) ) = [ ( 𝑝 ( .r ‘ 𝑂 ) 𝑞 ) ] ( 𝑂 ~QG 𝐼 ) )
33 5 2idllidld ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
34 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
35 1 34 lidlss ⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
36 33 35 syl ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
37 2 1 oppreqg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ⊆ 𝐵 ) → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )
38 4 36 37 syl2anc ⊢ ( 𝜑 → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )
39 38 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )
40 39 eceq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) = [ 𝑝 ] ( 𝑂 ~QG 𝐼 ) )
41 20 40 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑋 = [ 𝑝 ] ( 𝑂 ~QG 𝐼 ) )
42 39 eceq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) = [ 𝑞 ] ( 𝑂 ~QG 𝐼 ) )
43 19 42 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑌 = [ 𝑞 ] ( 𝑂 ~QG 𝐼 ) )
44 41 43 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑋 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) = ( [ 𝑝 ] ( 𝑂 ~QG 𝐼 ) ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑂 ~QG 𝐼 ) ) )
45 1 13 2 24 opprmul ⊢ ( 𝑝 ( .r ‘ 𝑂 ) 𝑞 ) = ( 𝑞 ( .r ‘ 𝑅 ) 𝑝 )
46 45 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑝 ( .r ‘ 𝑂 ) 𝑞 ) = ( 𝑞 ( .r ‘ 𝑅 ) 𝑝 ) )
47 46 eceq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → [ ( 𝑝 ( .r ‘ 𝑂 ) 𝑞 ) ] ( 𝑅 ~QG 𝐼 ) = [ ( 𝑞 ( .r ‘ 𝑅 ) 𝑝 ) ] ( 𝑅 ~QG 𝐼 ) )
48 39 eceq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → [ ( 𝑝 ( .r ‘ 𝑂 ) 𝑞 ) ] ( 𝑅 ~QG 𝐼 ) = [ ( 𝑝 ( .r ‘ 𝑂 ) 𝑞 ) ] ( 𝑂 ~QG 𝐼 ) )
49 47 48 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → [ ( 𝑞 ( .r ‘ 𝑅 ) 𝑝 ) ] ( 𝑅 ~QG 𝐼 ) = [ ( 𝑝 ( .r ‘ 𝑂 ) 𝑞 ) ] ( 𝑂 ~QG 𝐼 ) )
50 32 44 49 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑋 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) = [ ( 𝑞 ( .r ‘ 𝑅 ) 𝑝 ) ] ( 𝑅 ~QG 𝐼 ) )
51 18 21 50 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑌 ( .r ‘ 𝑄 ) 𝑋 ) = ( 𝑋 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) )
52 10 6 opprbas ⊢ 𝐸 = ( Base ‘ ( oppr ‘ 𝑄 ) )
53 8 52 eleqtrdi ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑌 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) )
55 3 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) )
56 1 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
57 ovexd ⊢ ( 𝜑 → ( 𝑅 ~QG 𝐼 ) ∈ V )
58 55 56 57 4 qusbas ⊢ ( 𝜑 → ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) = ( Base ‘ 𝑄 ) )
59 6 52 eqtr3i ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( oppr ‘ 𝑄 ) )
60 58 59 eqtr2di ⊢ ( 𝜑 → ( Base ‘ ( oppr ‘ 𝑄 ) ) = ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) )
61 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) → ( Base ‘ ( oppr ‘ 𝑄 ) ) = ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) )
62 54 61 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑌 ∈ ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) )
63 elqsi ⊢ ( 𝑌 ∈ ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) → ∃ 𝑞 ∈ 𝐵 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) )
64 62 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) → ∃ 𝑞 ∈ 𝐵 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) )
65 51 64 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑌 ( .r ‘ 𝑄 ) 𝑋 ) = ( 𝑋 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) )
66 7 52 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) )
67 66 60 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) )
68 elqsi ⊢ ( 𝑋 ∈ ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) → ∃ 𝑝 ∈ 𝐵 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) )
69 67 68 syl ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐵 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) )
70 65 69 r19.29a ⊢ ( 𝜑 → ( 𝑌 ( .r ‘ 𝑄 ) 𝑋 ) = ( 𝑋 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) )
71 12 70 eqtrid ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑌 ) = ( 𝑋 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) )