Step | Hyp | Ref
| Expression |
1 | | opprqusmulr.e |
. . 3
⊢ 𝐸 = (Base‘𝑄) |
2 | | eqid 2732 |
. . 3
⊢
(.r‘𝑄) = (.r‘𝑄) |
3 | | eqid 2732 |
. . 3
⊢
(oppr‘𝑄) = (oppr‘𝑄) |
4 | | eqid 2732 |
. . 3
⊢
(.r‘(oppr‘𝑄)) =
(.r‘(oppr‘𝑄)) |
5 | 1, 2, 3, 4 | opprmul 20107 |
. 2
⊢ (𝑋(.r‘(oppr‘𝑄))𝑌) = (𝑌(.r‘𝑄)𝑋) |
6 | | opprqus.q |
. . . . . 6
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) |
7 | | opprqus.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
8 | | eqid 2732 |
. . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) |
9 | | opprqus1r.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
10 | 9 | ad4antr 730 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑅 ∈ Ring) |
11 | | opprqus1r.i |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
12 | 11 | ad4antr 730 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝐼 ∈ (2Ideal‘𝑅)) |
13 | | simplr 767 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑞 ∈ 𝐵) |
14 | | simp-4r 782 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑝 ∈ 𝐵) |
15 | 6, 7, 8, 2, 10, 12, 13, 14 | qusmul2 20813 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → ([𝑞](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑝](𝑅 ~QG 𝐼)) = [(𝑞(.r‘𝑅)𝑝)](𝑅 ~QG 𝐼)) |
16 | | simpr 485 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑌 = [𝑞](𝑅 ~QG 𝐼)) |
17 | | simpllr 774 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑋 = [𝑝](𝑅 ~QG 𝐼)) |
18 | 16, 17 | oveq12d 7412 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑌(.r‘𝑄)𝑋) = ([𝑞](𝑅 ~QG 𝐼)(.r‘𝑄)[𝑝](𝑅 ~QG 𝐼))) |
19 | | eqid 2732 |
. . . . . . 7
⊢ (𝑂 /s (𝑂 ~QG 𝐼)) = (𝑂 /s (𝑂 ~QG 𝐼)) |
20 | | opprqus.o |
. . . . . . . 8
⊢ 𝑂 =
(oppr‘𝑅) |
21 | 20, 7 | opprbas 20111 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑂) |
22 | | eqid 2732 |
. . . . . . 7
⊢
(.r‘𝑂) = (.r‘𝑂) |
23 | | eqid 2732 |
. . . . . . 7
⊢
(.r‘(𝑂 /s (𝑂 ~QG 𝐼))) = (.r‘(𝑂 /s (𝑂 ~QG 𝐼))) |
24 | 20 | opprring 20115 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑂 ∈ Ring) |
25 | 9, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ Ring) |
26 | 25 | ad4antr 730 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑂 ∈ Ring) |
27 | 20, 9 | oppr2idl 32510 |
. . . . . . . . 9
⊢ (𝜑 → (2Ideal‘𝑅) = (2Ideal‘𝑂)) |
28 | 11, 27 | eleqtrd 2835 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑂)) |
29 | 28 | ad4antr 730 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝐼 ∈ (2Ideal‘𝑂)) |
30 | 19, 21, 22, 23, 26, 29, 14, 13 | qusmul2 20813 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → ([𝑝](𝑂 ~QG 𝐼)(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))[𝑞](𝑂 ~QG 𝐼)) = [(𝑝(.r‘𝑂)𝑞)](𝑂 ~QG 𝐼)) |
31 | 11 | 2idllidld 20807 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) |
32 | | eqid 2732 |
. . . . . . . . . . . . 13
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
33 | 7, 32 | lidlss 20783 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ (LIdeal‘𝑅) → 𝐼 ⊆ 𝐵) |
34 | 31, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ⊆ 𝐵) |
35 | 20, 7 | oppreqg 32507 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ⊆ 𝐵) → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼)) |
36 | 9, 34, 35 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼)) |
37 | 36 | ad4antr 730 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼)) |
38 | 37 | eceq2d 8730 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [𝑝](𝑅 ~QG 𝐼) = [𝑝](𝑂 ~QG 𝐼)) |
39 | 17, 38 | eqtrd 2772 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑋 = [𝑝](𝑂 ~QG 𝐼)) |
40 | 37 | eceq2d 8730 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [𝑞](𝑅 ~QG 𝐼) = [𝑞](𝑂 ~QG 𝐼)) |
41 | 16, 40 | eqtrd 2772 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → 𝑌 = [𝑞](𝑂 ~QG 𝐼)) |
42 | 39, 41 | oveq12d 7412 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌) = ([𝑝](𝑂 ~QG 𝐼)(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))[𝑞](𝑂 ~QG 𝐼))) |
43 | 7, 8, 20, 22 | opprmul 20107 |
. . . . . . . . 9
⊢ (𝑝(.r‘𝑂)𝑞) = (𝑞(.r‘𝑅)𝑝) |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑝(.r‘𝑂)𝑞) = (𝑞(.r‘𝑅)𝑝)) |
45 | 44 | eceq1d 8727 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [(𝑝(.r‘𝑂)𝑞)](𝑅 ~QG 𝐼) = [(𝑞(.r‘𝑅)𝑝)](𝑅 ~QG 𝐼)) |
46 | 37 | eceq2d 8730 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [(𝑝(.r‘𝑂)𝑞)](𝑅 ~QG 𝐼) = [(𝑝(.r‘𝑂)𝑞)](𝑂 ~QG 𝐼)) |
47 | 45, 46 | eqtr3d 2774 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → [(𝑞(.r‘𝑅)𝑝)](𝑅 ~QG 𝐼) = [(𝑝(.r‘𝑂)𝑞)](𝑂 ~QG 𝐼)) |
48 | 30, 42, 47 | 3eqtr4d 2782 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌) = [(𝑞(.r‘𝑅)𝑝)](𝑅 ~QG 𝐼)) |
49 | 15, 18, 48 | 3eqtr4d 2782 |
. . . 4
⊢
(((((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) ∧ 𝑞 ∈ 𝐵) ∧ 𝑌 = [𝑞](𝑅 ~QG 𝐼)) → (𝑌(.r‘𝑄)𝑋) = (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) |
50 | | opprqusmulr.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝐸) |
51 | 3, 1 | opprbas 20111 |
. . . . . . . 8
⊢ 𝐸 =
(Base‘(oppr‘𝑄)) |
52 | 50, 51 | eleqtrdi 2843 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈
(Base‘(oppr‘𝑄))) |
53 | 52 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) → 𝑌 ∈
(Base‘(oppr‘𝑄))) |
54 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))) |
55 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
56 | | ovexd 7429 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ~QG 𝐼) ∈ V) |
57 | 54, 55, 56, 9 | qusbas 17475 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 / (𝑅 ~QG 𝐼)) = (Base‘𝑄)) |
58 | 1, 51 | eqtr3i 2762 |
. . . . . . . 8
⊢
(Base‘𝑄) =
(Base‘(oppr‘𝑄)) |
59 | 57, 58 | eqtr2di 2789 |
. . . . . . 7
⊢ (𝜑 →
(Base‘(oppr‘𝑄)) = (𝐵 / (𝑅 ~QG 𝐼))) |
60 | 59 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) →
(Base‘(oppr‘𝑄)) = (𝐵 / (𝑅 ~QG 𝐼))) |
61 | 53, 60 | eleqtrd 2835 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ 𝐵) ∧ 𝑋 = [𝑝](𝑅 ~QG 𝐼)) → 𝑌 ∈ (𝐵 / (𝑅 ~QG 𝐼))) |
62 | | elqsi 8749 |
. . . . 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 2843 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈
(Base‘(oppr‘𝑄))) |
67 | 66, 59 | eleqtrd 2835 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐵 / (𝑅 ~QG 𝐼))) |
68 | | elqsi 8749 |
. . . 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 2784 |
1
⊢ (𝜑 → (𝑋(.r‘(oppr‘𝑄))𝑌) = (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) |