Proof of Theorem crngpropd
| Step | Hyp | Ref
 | Expression | 
| 1 |   | ringpropd.1 | 
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) | 
| 2 |   | eqid 2196 | 
. . . . . . 7
⊢
(mulGrp‘𝐾) =
(mulGrp‘𝐾) | 
| 3 |   | eqid 2196 | 
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 4 | 2, 3 | mgpbasg 13482 | 
. . . . . 6
⊢ (𝐾 ∈ Ring →
(Base‘𝐾) =
(Base‘(mulGrp‘𝐾))) | 
| 5 | 1, 4 | sylan9eq 2249 | 
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ Ring) → 𝐵 = (Base‘(mulGrp‘𝐾))) | 
| 6 |   | ringpropd.2 | 
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) | 
| 7 | 6 | adantr 276 | 
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ Ring) → 𝐵 = (Base‘𝐿)) | 
| 8 |   | ringpropd.3 | 
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) | 
| 9 |   | ringpropd.4 | 
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) | 
| 10 | 1, 6, 8, 9 | ringpropd 13594 | 
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∈ Ring ↔ 𝐿 ∈ Ring)) | 
| 11 | 10 | biimpa 296 | 
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ Ring) → 𝐿 ∈ Ring) | 
| 12 |   | eqid 2196 | 
. . . . . . . 8
⊢
(mulGrp‘𝐿) =
(mulGrp‘𝐿) | 
| 13 |   | eqid 2196 | 
. . . . . . . 8
⊢
(Base‘𝐿) =
(Base‘𝐿) | 
| 14 | 12, 13 | mgpbasg 13482 | 
. . . . . . 7
⊢ (𝐿 ∈ Ring →
(Base‘𝐿) =
(Base‘(mulGrp‘𝐿))) | 
| 15 | 11, 14 | syl 14 | 
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ Ring) → (Base‘𝐿) =
(Base‘(mulGrp‘𝐿))) | 
| 16 | 7, 15 | eqtrd 2229 | 
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ Ring) → 𝐵 = (Base‘(mulGrp‘𝐿))) | 
| 17 | 9 | adantlr 477 | 
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) | 
| 18 |   | eqid 2196 | 
. . . . . . . . 9
⊢
(.r‘𝐾) = (.r‘𝐾) | 
| 19 | 2, 18 | mgpplusgg 13480 | 
. . . . . . . 8
⊢ (𝐾 ∈ Ring →
(.r‘𝐾) =
(+g‘(mulGrp‘𝐾))) | 
| 20 | 19 | adantl 277 | 
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ Ring) →
(.r‘𝐾) =
(+g‘(mulGrp‘𝐾))) | 
| 21 | 20 | oveqdr 5950 | 
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(+g‘(mulGrp‘𝐾))𝑦)) | 
| 22 |   | eqid 2196 | 
. . . . . . . . 9
⊢
(.r‘𝐿) = (.r‘𝐿) | 
| 23 | 12, 22 | mgpplusgg 13480 | 
. . . . . . . 8
⊢ (𝐿 ∈ Ring →
(.r‘𝐿) =
(+g‘(mulGrp‘𝐿))) | 
| 24 | 11, 23 | syl 14 | 
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ Ring) →
(.r‘𝐿) =
(+g‘(mulGrp‘𝐿))) | 
| 25 | 24 | oveqdr 5950 | 
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐿)𝑦) = (𝑥(+g‘(mulGrp‘𝐿))𝑦)) | 
| 26 | 17, 21, 25 | 3eqtr3d 2237 | 
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘(mulGrp‘𝐾))𝑦) = (𝑥(+g‘(mulGrp‘𝐿))𝑦)) | 
| 27 | 5, 16, 26 | cmnpropd 13425 | 
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ Ring) → ((mulGrp‘𝐾) ∈ CMnd ↔
(mulGrp‘𝐿) ∈
CMnd)) | 
| 28 | 27 | pm5.32da 452 | 
. . 3
⊢ (𝜑 → ((𝐾 ∈ Ring ∧ (mulGrp‘𝐾) ∈ CMnd) ↔ (𝐾 ∈ Ring ∧
(mulGrp‘𝐿) ∈
CMnd))) | 
| 29 | 10 | anbi1d 465 | 
. . 3
⊢ (𝜑 → ((𝐾 ∈ Ring ∧ (mulGrp‘𝐿) ∈ CMnd) ↔ (𝐿 ∈ Ring ∧
(mulGrp‘𝐿) ∈
CMnd))) | 
| 30 | 28, 29 | bitrd 188 | 
. 2
⊢ (𝜑 → ((𝐾 ∈ Ring ∧ (mulGrp‘𝐾) ∈ CMnd) ↔ (𝐿 ∈ Ring ∧
(mulGrp‘𝐿) ∈
CMnd))) | 
| 31 | 2 | iscrng 13559 | 
. 2
⊢ (𝐾 ∈ CRing ↔ (𝐾 ∈ Ring ∧
(mulGrp‘𝐾) ∈
CMnd)) | 
| 32 | 12 | iscrng 13559 | 
. 2
⊢ (𝐿 ∈ CRing ↔ (𝐿 ∈ Ring ∧
(mulGrp‘𝐿) ∈
CMnd)) | 
| 33 | 30, 31, 32 | 3bitr4g 223 | 
1
⊢ (𝜑 → (𝐾 ∈ CRing ↔ 𝐿 ∈ CRing)) |