Step | Hyp | Ref
| Expression |
1 | | unitpropdg.1 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
2 | | unitpropdg.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
3 | | unitpropdg.3 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) |
4 | | unitpropdg.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Ring) |
5 | | unitpropdg.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ Ring) |
6 | 1, 2, 3, 4, 5 | rngidpropdg 13268 |
. . . . . 6
⊢ (𝜑 → (1r‘𝐾) = (1r‘𝐿)) |
7 | 6 | breq2d 4015 |
. . . . 5
⊢ (𝜑 → (𝑧(∥r‘𝐾)(1r‘𝐾) ↔ 𝑧(∥r‘𝐾)(1r‘𝐿))) |
8 | 6 | breq2d 4015 |
. . . . 5
⊢ (𝜑 → (𝑧(∥r‘(oppr‘𝐾))(1r‘𝐾) ↔ 𝑧(∥r‘(oppr‘𝐾))(1r‘𝐿))) |
9 | 7, 8 | anbi12d 473 |
. . . 4
⊢ (𝜑 → ((𝑧(∥r‘𝐾)(1r‘𝐾) ∧ 𝑧(∥r‘(oppr‘𝐾))(1r‘𝐾)) ↔ (𝑧(∥r‘𝐾)(1r‘𝐿) ∧ 𝑧(∥r‘(oppr‘𝐾))(1r‘𝐿)))) |
10 | | ringsrg 13177 |
. . . . . . . 8
⊢ (𝐾 ∈ Ring → 𝐾 ∈ SRing) |
11 | 4, 10 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ SRing) |
12 | | ringsrg 13177 |
. . . . . . . 8
⊢ (𝐿 ∈ Ring → 𝐿 ∈ SRing) |
13 | 5, 12 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ SRing) |
14 | 1, 2, 3, 11, 13 | dvdsrpropdg 13269 |
. . . . . 6
⊢ (𝜑 →
(∥r‘𝐾) = (∥r‘𝐿)) |
15 | 14 | breqd 4014 |
. . . . 5
⊢ (𝜑 → (𝑧(∥r‘𝐾)(1r‘𝐿) ↔ 𝑧(∥r‘𝐿)(1r‘𝐿))) |
16 | | eqid 2177 |
. . . . . . . . . 10
⊢
(oppr‘𝐾) = (oppr‘𝐾) |
17 | | eqid 2177 |
. . . . . . . . . 10
⊢
(Base‘𝐾) =
(Base‘𝐾) |
18 | 16, 17 | opprbasg 13200 |
. . . . . . . . 9
⊢ (𝐾 ∈ Ring →
(Base‘𝐾) =
(Base‘(oppr‘𝐾))) |
19 | 4, 18 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐾) =
(Base‘(oppr‘𝐾))) |
20 | 1, 19 | eqtrd 2210 |
. . . . . . 7
⊢ (𝜑 → 𝐵 =
(Base‘(oppr‘𝐾))) |
21 | | eqid 2177 |
. . . . . . . . . 10
⊢
(oppr‘𝐿) = (oppr‘𝐿) |
22 | | eqid 2177 |
. . . . . . . . . 10
⊢
(Base‘𝐿) =
(Base‘𝐿) |
23 | 21, 22 | opprbasg 13200 |
. . . . . . . . 9
⊢ (𝐿 ∈ Ring →
(Base‘𝐿) =
(Base‘(oppr‘𝐿))) |
24 | 5, 23 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐿) =
(Base‘(oppr‘𝐿))) |
25 | 2, 24 | eqtrd 2210 |
. . . . . . 7
⊢ (𝜑 → 𝐵 =
(Base‘(oppr‘𝐿))) |
26 | 3 | ancom2s 566 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) |
27 | 4 | adantr 276 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → 𝐾 ∈ Ring) |
28 | | simprl 529 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
29 | | simprr 531 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
30 | | eqid 2177 |
. . . . . . . . . 10
⊢
(.r‘𝐾) = (.r‘𝐾) |
31 | | eqid 2177 |
. . . . . . . . . 10
⊢
(.r‘(oppr‘𝐾)) =
(.r‘(oppr‘𝐾)) |
32 | 17, 30, 16, 31 | opprmulg 13196 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑦(.r‘(oppr‘𝐾))𝑥) = (𝑥(.r‘𝐾)𝑦)) |
33 | 27, 28, 29, 32 | syl3anc 1238 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑦(.r‘(oppr‘𝐾))𝑥) = (𝑥(.r‘𝐾)𝑦)) |
34 | 5 | adantr 276 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → 𝐿 ∈ Ring) |
35 | | eqid 2177 |
. . . . . . . . . 10
⊢
(.r‘𝐿) = (.r‘𝐿) |
36 | | eqid 2177 |
. . . . . . . . . 10
⊢
(.r‘(oppr‘𝐿)) =
(.r‘(oppr‘𝐿)) |
37 | 22, 35, 21, 36 | opprmulg 13196 |
. . . . . . . . 9
⊢ ((𝐿 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑦(.r‘(oppr‘𝐿))𝑥) = (𝑥(.r‘𝐿)𝑦)) |
38 | 34, 28, 29, 37 | syl3anc 1238 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑦(.r‘(oppr‘𝐿))𝑥) = (𝑥(.r‘𝐿)𝑦)) |
39 | 26, 33, 38 | 3eqtr4d 2220 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑦(.r‘(oppr‘𝐾))𝑥) = (𝑦(.r‘(oppr‘𝐿))𝑥)) |
40 | 16 | opprring 13202 |
. . . . . . . 8
⊢ (𝐾 ∈ Ring →
(oppr‘𝐾) ∈ Ring) |
41 | | ringsrg 13177 |
. . . . . . . 8
⊢
((oppr‘𝐾) ∈ Ring →
(oppr‘𝐾) ∈ SRing) |
42 | 4, 40, 41 | 3syl 17 |
. . . . . . 7
⊢ (𝜑 →
(oppr‘𝐾) ∈ SRing) |
43 | 21 | opprring 13202 |
. . . . . . . 8
⊢ (𝐿 ∈ Ring →
(oppr‘𝐿) ∈ Ring) |
44 | | ringsrg 13177 |
. . . . . . . 8
⊢
((oppr‘𝐿) ∈ Ring →
(oppr‘𝐿) ∈ SRing) |
45 | 5, 43, 44 | 3syl 17 |
. . . . . . 7
⊢ (𝜑 →
(oppr‘𝐿) ∈ SRing) |
46 | 20, 25, 39, 42, 45 | dvdsrpropdg 13269 |
. . . . . 6
⊢ (𝜑 →
(∥r‘(oppr‘𝐾)) =
(∥r‘(oppr‘𝐿))) |
47 | 46 | breqd 4014 |
. . . . 5
⊢ (𝜑 → (𝑧(∥r‘(oppr‘𝐾))(1r‘𝐿) ↔ 𝑧(∥r‘(oppr‘𝐿))(1r‘𝐿))) |
48 | 15, 47 | anbi12d 473 |
. . . 4
⊢ (𝜑 → ((𝑧(∥r‘𝐾)(1r‘𝐿) ∧ 𝑧(∥r‘(oppr‘𝐾))(1r‘𝐿)) ↔ (𝑧(∥r‘𝐿)(1r‘𝐿) ∧ 𝑧(∥r‘(oppr‘𝐿))(1r‘𝐿)))) |
49 | 9, 48 | bitrd 188 |
. . 3
⊢ (𝜑 → ((𝑧(∥r‘𝐾)(1r‘𝐾) ∧ 𝑧(∥r‘(oppr‘𝐾))(1r‘𝐾)) ↔ (𝑧(∥r‘𝐿)(1r‘𝐿) ∧ 𝑧(∥r‘(oppr‘𝐿))(1r‘𝐿)))) |
50 | | eqidd 2178 |
. . . 4
⊢ (𝜑 → (Unit‘𝐾) = (Unit‘𝐾)) |
51 | | eqidd 2178 |
. . . 4
⊢ (𝜑 → (1r‘𝐾) = (1r‘𝐾)) |
52 | | eqidd 2178 |
. . . 4
⊢ (𝜑 →
(∥r‘𝐾) = (∥r‘𝐾)) |
53 | | eqidd 2178 |
. . . 4
⊢ (𝜑 →
(oppr‘𝐾) = (oppr‘𝐾)) |
54 | | eqidd 2178 |
. . . 4
⊢ (𝜑 →
(∥r‘(oppr‘𝐾)) =
(∥r‘(oppr‘𝐾))) |
55 | 50, 51, 52, 53, 54, 11 | isunitd 13228 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (Unit‘𝐾) ↔ (𝑧(∥r‘𝐾)(1r‘𝐾) ∧ 𝑧(∥r‘(oppr‘𝐾))(1r‘𝐾)))) |
56 | | eqidd 2178 |
. . . 4
⊢ (𝜑 → (Unit‘𝐿) = (Unit‘𝐿)) |
57 | | eqidd 2178 |
. . . 4
⊢ (𝜑 → (1r‘𝐿) = (1r‘𝐿)) |
58 | | eqidd 2178 |
. . . 4
⊢ (𝜑 →
(∥r‘𝐿) = (∥r‘𝐿)) |
59 | | eqidd 2178 |
. . . 4
⊢ (𝜑 →
(oppr‘𝐿) = (oppr‘𝐿)) |
60 | | eqidd 2178 |
. . . 4
⊢ (𝜑 →
(∥r‘(oppr‘𝐿)) =
(∥r‘(oppr‘𝐿))) |
61 | 56, 57, 58, 59, 60, 13 | isunitd 13228 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (Unit‘𝐿) ↔ (𝑧(∥r‘𝐿)(1r‘𝐿) ∧ 𝑧(∥r‘(oppr‘𝐿))(1r‘𝐿)))) |
62 | 49, 55, 61 | 3bitr4d 220 |
. 2
⊢ (𝜑 → (𝑧 ∈ (Unit‘𝐾) ↔ 𝑧 ∈ (Unit‘𝐿))) |
63 | 62 | eqrdv 2175 |
1
⊢ (𝜑 → (Unit‘𝐾) = (Unit‘𝐿)) |