| Step | Hyp | Ref
| Expression |
| 1 | | opprqusmulr.e |
. . 3
⊢ 𝐸 = (Base‘𝑄) |
| 2 | | eqid 2737 |
. . 3
⊢
(.r‘𝑄) = (.r‘𝑄) |
| 3 | | eqid 2737 |
. . 3
⊢
(oppr‘𝑄) = (oppr‘𝑄) |
| 4 | | eqid 2737 |
. . 3
⊢
(.r‘(oppr‘𝑄)) =
(.r‘(oppr‘𝑄)) |
| 5 | 1, 2, 3, 4 | opprmul 20337 |
. 2
⊢ (𝑋(.r‘(oppr‘𝑄))𝑌) = (𝑌(.r‘𝑄)𝑋) |
| 6 | | opprqus.q |
. . . . . 6
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) |
| 7 | | opprqus.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 8 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 9 | | opprqus1r.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 10 | 9 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑅 ∈ Ring) |
| 11 | | opprqus1r.i |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
| 12 | 11 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝐼 ∈ (2Ideal‘𝑅)) |
| 13 | | simplr 769 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑞 ∈ 𝐵) |
| 14 | | simp-4r 784 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑝 ∈ 𝐵) |
| 15 | 6, 7, 8, 2, 10, 12, 13, 14 | qusmul2idl 21289 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → ([𝑞](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑝](𝑅 ~QG 𝐼)) = [(𝑞(.r‘𝑅)𝑝)](𝑅 ~QG 𝐼)) |
| 16 | | simpr 484 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑌 = [𝑞](𝑅 ~QG 𝐼)) |
| 17 | | simpllr 776 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑋 = [𝑝](𝑅 ~QG 𝐼)) |
| 18 | 16, 17 | oveq12d 7449 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑌(.r‘𝑄)𝑋) = ([𝑞](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑝](𝑅 ~QG 𝐼))) |
| 19 | | eqid 2737 |
. . . . . . 7
⊢ (𝑂 /s (𝑂 ~QG 𝐼)) = (𝑂 /s (𝑂 ~QG 𝐼)) |
| 20 | | opprqus.o |
. . . . . . . 8
⊢ 𝑂 =
(oppr‘𝑅) |
| 21 | 20, 7 | opprbas 20341 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑂) |
| 22 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑂) = (.r‘𝑂) |
| 23 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘(𝑂 /s (𝑂 ~QG 𝐼))) = (.r‘(𝑂 /s (𝑂 ~QG 𝐼))) |
| 24 | 20 | opprring 20347 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑂 ∈ Ring) |
| 25 | 9, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ Ring) |
| 26 | 25 | ad4antr 732 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑂 ∈ Ring) |
| 27 | 20, 9 | oppr2idl 33514 |
. . . . . . . . 9
⊢ (𝜑 → (2Ideal‘𝑅) = (2Ideal‘𝑂)) |
| 28 | 11, 27 | eleqtrd 2843 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑂)) |
| 29 | 28 | ad4antr 732 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝐼 ∈ (2Ideal‘𝑂)) |
| 30 | 19, 21, 22, 23, 26, 29, 14, 13 | qusmul2idl 21289 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → ([𝑝](𝑂 ~QG 𝐼)(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))[𝑞](𝑂 ~QG 𝐼)) = [(𝑝(.r‘𝑂)𝑞)](𝑂 ~QG 𝐼)) |
| 31 | 11 | 2idllidld 21264 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) |
| 32 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
| 33 | 7, 32 | lidlss 21222 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ (LIdeal‘𝑅) → 𝐼 ⊆ 𝐵) |
| 34 | 31, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ⊆ 𝐵) |
| 35 | 20, 7 | oppreqg 33511 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ⊆ 𝐵) → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼)) |
| 36 | 9, 34, 35 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼)) |
| 37 | 36 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼)) |
| 38 | 37 | eceq2d 8788 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [𝑝](𝑅 ~QG 𝐼) = [𝑝](𝑂 ~QG 𝐼)) |
| 39 | 17, 38 | eqtrd 2777 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑋 = [𝑝](𝑂 ~QG 𝐼)) |
| 40 | 37 | eceq2d 8788 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [𝑞](𝑅 ~QG 𝐼) = [𝑞](𝑂 ~QG 𝐼)) |
| 41 | 16, 40 | eqtrd 2777 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑌 = [𝑞](𝑂 ~QG 𝐼)) |
| 42 | 39, 41 | oveq12d 7449 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌) = ([𝑝](𝑂 ~QG 𝐼)(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))[𝑞](𝑂 ~QG 𝐼))) |
| 43 | 7, 8, 20, 22 | opprmul 20337 |
. . . . . . . . 9
⊢ (𝑝(.r‘𝑂)𝑞) = (𝑞(.r‘𝑅)𝑝) |
| 44 | 43 | a1i 11 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑝(.r‘𝑂)𝑞) = (𝑞(.r‘𝑅)𝑝)) |
| 45 | 44 | eceq1d 8785 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [(𝑝(.r‘𝑂)𝑞)](𝑅 ~QG 𝐼) = [(𝑞(.r‘𝑅)𝑝)](𝑅 ~QG 𝐼)) |
| 46 | 37 | eceq2d 8788 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [(𝑝(.r‘𝑂)𝑞)](𝑅 ~QG 𝐼) = [(𝑝(.r‘𝑂)𝑞)](𝑂 ~QG 𝐼)) |
| 47 | 45, 46 | eqtr3d 2779 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [(𝑞(.r‘𝑅)𝑝)](𝑅 ~QG 𝐼) = [(𝑝(.r‘𝑂)𝑞)](𝑂 ~QG 𝐼)) |
| 48 | 30, 42, 47 | 3eqtr4d 2787 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌) = [(𝑞(.r‘𝑅)𝑝)](𝑅 ~QG 𝐼)) |
| 49 | 15, 18, 48 | 3eqtr4d 2787 |
. . . 4
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑌(.r‘𝑄)𝑋) = (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) |
| 50 | | opprqusmulr.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝐸) |
| 51 | 3, 1 | opprbas 20341 |
. . . . . . . 8
⊢ 𝐸 =
(Base‘(oppr‘𝑄)) |
| 52 | 50, 51 | eleqtrdi 2851 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈
(Base‘(oppr‘𝑄))) |
| 53 | 52 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) → 𝑌 ∈
(Base‘(oppr‘𝑄))) |
| 54 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))) |
| 55 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
| 56 | | ovexd 7466 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ~QG 𝐼) ∈ V) |
| 57 | 54, 55, 56, 9 | qusbas 17590 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 / (𝑅 ~QG 𝐼)) = (Base‘𝑄)) |
| 58 | 1, 51 | eqtr3i 2767 |
. . . . . . . 8
⊢
(Base‘𝑄) =
(Base‘(oppr‘𝑄)) |
| 59 | 57, 58 | eqtr2di 2794 |
. . . . . . 7
⊢ (𝜑 →
(Base‘(oppr‘𝑄)) = (𝐵 / (𝑅 ~QG 𝐼))) |
| 60 | 59 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) →
(Base‘(oppr‘𝑄)) = (𝐵 / (𝑅 ~QG 𝐼))) |
| 61 | 53, 60 | eleqtrd 2843 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) → 𝑌 ∈ (𝐵 / (𝑅 ~QG 𝐼))) |
| 62 | | elqsi 8810 |
. . . . 5
⊢ (𝑌 ∈ (𝐵 / (𝑅 ~QG 𝐼)) → ∃𝑞 ∈ 𝐵 𝑌 = [𝑞](𝑅 ~QG 𝐼)) |
| 63 | 61, 62 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) → ∃𝑞 ∈ 𝐵 𝑌 = [𝑞](𝑅 ~QG 𝐼)) |
| 64 | 49, 63 | r19.29a 3162 |
. . 3
⊢ (((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) → (𝑌(.r‘𝑄)𝑋) = (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) |
| 65 | | opprqusmulr.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐸) |
| 66 | 65, 51 | eleqtrdi 2851 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈
(Base‘(oppr‘𝑄))) |
| 67 | 66, 59 | eleqtrd 2843 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐵 / (𝑅 ~QG 𝐼))) |
| 68 | | elqsi 8810 |
. . . 4
⊢ (𝑋 ∈ (𝐵 / (𝑅 ~QG 𝐼)) → ∃𝑝 ∈ 𝐵 𝑋 = [𝑝](𝑅 ~QG 𝐼)) |
| 69 | 67, 68 | syl 17 |
. . 3
⊢ (𝜑 → ∃𝑝 ∈ 𝐵 𝑋 = [𝑝](𝑅 ~QG 𝐼)) |
| 70 | 64, 69 | r19.29a 3162 |
. 2
⊢ (𝜑 → (𝑌(.r‘𝑄)𝑋) = (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) |
| 71 | 5, 70 | eqtrid 2789 |
1
⊢ (𝜑 → (𝑋(.r‘(oppr‘𝑄))𝑌) = (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) |