| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fracval 33307 | . 2
⊢ ( Frac
‘𝑅) = (𝑅 RLocal (RLReg‘𝑅)) | 
| 2 |  | fracfld.1 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ IDomn) | 
| 3 | 2 | idomdomd 20727 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Domn) | 
| 4 |  | domnnzr 20707 | . . . . . . 7
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | 
| 5 |  | eqid 2736 | . . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 6 |  | eqid 2736 | . . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 7 | 5, 6 | nzrnz 20516 | . . . . . . 7
⊢ (𝑅 ∈ NzRing →
(1r‘𝑅)
≠ (0g‘𝑅)) | 
| 8 | 3, 4, 7 | 3syl 18 | . . . . . 6
⊢ (𝜑 → (1r‘𝑅) ≠
(0g‘𝑅)) | 
| 9 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢
(1r‘𝑅) ∈ V | 
| 10 | 9, 9 | op1st 8023 | . . . . . . . . . . . . . . . 16
⊢
(1st ‘〈(1r‘𝑅), (1r‘𝑅)〉) = (1r‘𝑅) | 
| 11 | 10 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (1st
‘〈(1r‘𝑅), (1r‘𝑅)〉) = (1r‘𝑅)) | 
| 12 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑅) ∈ V | 
| 13 | 12, 9 | op2nd 8024 | . . . . . . . . . . . . . . . 16
⊢
(2nd ‘〈(0g‘𝑅), (1r‘𝑅)〉) = (1r‘𝑅) | 
| 14 | 13 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉) = (1r‘𝑅)) | 
| 15 | 11, 14 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉)) = ((1r‘𝑅)(.r‘𝑅)(1r‘𝑅))) | 
| 16 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 17 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 18 | 2 | idomringd 20729 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 19 | 18 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → 𝑅 ∈ Ring) | 
| 20 | 16, 5 | ringidcl 20263 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) | 
| 21 | 19, 20 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 22 | 16, 17, 5, 19, 21 | ringlidmd 20270 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) | 
| 23 | 15, 22 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉)) = (1r‘𝑅)) | 
| 24 | 12, 9 | op1st 8023 | . . . . . . . . . . . . . . . 16
⊢
(1st ‘〈(0g‘𝑅), (1r‘𝑅)〉) = (0g‘𝑅) | 
| 25 | 24 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (1st
‘〈(0g‘𝑅), (1r‘𝑅)〉) = (0g‘𝑅)) | 
| 26 | 9, 9 | op2nd 8024 | . . . . . . . . . . . . . . . 16
⊢
(2nd ‘〈(1r‘𝑅), (1r‘𝑅)〉) = (1r‘𝑅) | 
| 27 | 26 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉) = (1r‘𝑅)) | 
| 28 | 25, 27 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉)) = ((0g‘𝑅)(.r‘𝑅)(1r‘𝑅))) | 
| 29 | 18 | ringgrpd 20240 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 ∈ Grp) | 
| 30 | 16, 6 | grpidcl 18984 | . . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Grp →
(0g‘𝑅)
∈ (Base‘𝑅)) | 
| 31 | 29, 30 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅)) | 
| 32 | 31 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (0g‘𝑅) ∈ (Base‘𝑅)) | 
| 33 | 16, 17, 5, 19, 32 | ringridmd 20271 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (0g‘𝑅)) | 
| 34 | 28, 33 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉)) = (0g‘𝑅)) | 
| 35 | 23, 34 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉))(-g‘𝑅)((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉))) = ((1r‘𝑅)(-g‘𝑅)(0g‘𝑅))) | 
| 36 | 35 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (𝑡(.r‘𝑅)(((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉))(-g‘𝑅)((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉)))) = (𝑡(.r‘𝑅)((1r‘𝑅)(-g‘𝑅)(0g‘𝑅)))) | 
| 37 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(-g‘𝑅) = (-g‘𝑅) | 
| 38 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(RLReg‘𝑅) =
(RLReg‘𝑅) | 
| 39 | 38, 16 | rrgss 20703 | . . . . . . . . . . . . . 14
⊢
(RLReg‘𝑅)
⊆ (Base‘𝑅) | 
| 40 | 39 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) → (RLReg‘𝑅) ⊆ (Base‘𝑅)) | 
| 41 | 40 | sselda 3982 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → 𝑡 ∈ (Base‘𝑅)) | 
| 42 | 16, 17, 37, 19, 41, 21, 32 | ringsubdi 20305 | . . . . . . . . . . 11
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (𝑡(.r‘𝑅)((1r‘𝑅)(-g‘𝑅)(0g‘𝑅))) = ((𝑡(.r‘𝑅)(1r‘𝑅))(-g‘𝑅)(𝑡(.r‘𝑅)(0g‘𝑅)))) | 
| 43 | 16, 17, 5, 19, 41 | ringridmd 20271 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (𝑡(.r‘𝑅)(1r‘𝑅)) = 𝑡) | 
| 44 | 16, 17, 6, 19, 41 | ringrzd 20294 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (𝑡(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) | 
| 45 | 43, 44 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ((𝑡(.r‘𝑅)(1r‘𝑅))(-g‘𝑅)(𝑡(.r‘𝑅)(0g‘𝑅))) = (𝑡(-g‘𝑅)(0g‘𝑅))) | 
| 46 | 29 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → 𝑅 ∈ Grp) | 
| 47 | 16, 6, 37 | grpsubid1 19044 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Grp ∧ 𝑡 ∈ (Base‘𝑅)) → (𝑡(-g‘𝑅)(0g‘𝑅)) = 𝑡) | 
| 48 | 46, 41, 47 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (𝑡(-g‘𝑅)(0g‘𝑅)) = 𝑡) | 
| 49 | 45, 48 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ((𝑡(.r‘𝑅)(1r‘𝑅))(-g‘𝑅)(𝑡(.r‘𝑅)(0g‘𝑅))) = 𝑡) | 
| 50 | 36, 42, 49 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → (𝑡(.r‘𝑅)(((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉))(-g‘𝑅)((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉)))) = 𝑡) | 
| 51 | 50 | eqeq1d 2738 | . . . . . . . . 9
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ((𝑡(.r‘𝑅)(((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉))(-g‘𝑅)((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉)))) = (0g‘𝑅) ↔ 𝑡 = (0g‘𝑅))) | 
| 52 | 51 | biimpa 476 | . . . . . . . 8
⊢ ((((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) ∧ (𝑡(.r‘𝑅)(((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉))(-g‘𝑅)((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉)))) = (0g‘𝑅)) → 𝑡 = (0g‘𝑅)) | 
| 53 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → 𝑡 ∈ (RLReg‘𝑅)) | 
| 54 | 38, 6 | rrgnz 20705 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ NzRing → ¬
(0g‘𝑅)
∈ (RLReg‘𝑅)) | 
| 55 | 3, 4, 54 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → ¬
(0g‘𝑅)
∈ (RLReg‘𝑅)) | 
| 56 | 55 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → ¬ (0g‘𝑅) ∈ (RLReg‘𝑅)) | 
| 57 |  | nelne2 3039 | . . . . . . . . . 10
⊢ ((𝑡 ∈ (RLReg‘𝑅) ∧ ¬
(0g‘𝑅)
∈ (RLReg‘𝑅))
→ 𝑡 ≠
(0g‘𝑅)) | 
| 58 | 53, 56, 57 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) → 𝑡 ≠ (0g‘𝑅)) | 
| 59 | 58 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) ∧ (𝑡(.r‘𝑅)(((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉))(-g‘𝑅)((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉)))) = (0g‘𝑅)) → 𝑡 ≠ (0g‘𝑅)) | 
| 60 | 52, 59 | pm2.21ddne 3025 | . . . . . . 7
⊢ ((((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑡 ∈ (RLReg‘𝑅)) ∧ (𝑡(.r‘𝑅)(((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉))(-g‘𝑅)((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉)))) = (0g‘𝑅)) →
(1r‘𝑅) =
(0g‘𝑅)) | 
| 61 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑅 ~RL
(RLReg‘𝑅)) = (𝑅 ~RL
(RLReg‘𝑅)) | 
| 62 |  | eqid 2736 | . . . . . . . . . . 11
⊢
((Base‘𝑅)
× (RLReg‘𝑅)) =
((Base‘𝑅) ×
(RLReg‘𝑅)) | 
| 63 | 2 | idomcringd 20728 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 64 | 16, 38, 6 | isdomn6 20715 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧
((Base‘𝑅) ∖
{(0g‘𝑅)})
= (RLReg‘𝑅))) | 
| 65 | 3, 64 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 ∈ NzRing ∧ ((Base‘𝑅) ∖
{(0g‘𝑅)})
= (RLReg‘𝑅))) | 
| 66 | 65 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → ((Base‘𝑅) ∖
{(0g‘𝑅)})
= (RLReg‘𝑅)) | 
| 67 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) | 
| 68 | 16, 6, 67 | isdomn3 20716 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧
((Base‘𝑅) ∖
{(0g‘𝑅)})
∈ (SubMnd‘(mulGrp‘𝑅)))) | 
| 69 | 3, 68 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 ∈ Ring ∧ ((Base‘𝑅) ∖
{(0g‘𝑅)})
∈ (SubMnd‘(mulGrp‘𝑅)))) | 
| 70 | 69 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → ((Base‘𝑅) ∖
{(0g‘𝑅)})
∈ (SubMnd‘(mulGrp‘𝑅))) | 
| 71 | 66, 70 | eqeltrrd 2841 | . . . . . . . . . . 11
⊢ (𝜑 → (RLReg‘𝑅) ∈
(SubMnd‘(mulGrp‘𝑅))) | 
| 72 | 16, 6, 5, 17, 37, 62, 61, 63, 71 | erler 33270 | . . . . . . . . . 10
⊢ (𝜑 → (𝑅 ~RL (RLReg‘𝑅)) Er ((Base‘𝑅) × (RLReg‘𝑅))) | 
| 73 | 18, 20 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 74 | 5, 38, 18 | 1rrg 33287 | . . . . . . . . . . 11
⊢ (𝜑 → (1r‘𝑅) ∈ (RLReg‘𝑅)) | 
| 75 | 73, 74 | opelxpd 5723 | . . . . . . . . . 10
⊢ (𝜑 →
〈(1r‘𝑅), (1r‘𝑅)〉 ∈ ((Base‘𝑅) × (RLReg‘𝑅))) | 
| 76 | 72, 75 | erth 8797 | . . . . . . . . 9
⊢ (𝜑 →
(〈(1r‘𝑅), (1r‘𝑅)〉(𝑅 ~RL (RLReg‘𝑅))〈(0g‘𝑅), (1r‘𝑅)〉 ↔
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))) | 
| 77 | 76 | biimpar 477 | . . . . . . . 8
⊢ ((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) →
〈(1r‘𝑅), (1r‘𝑅)〉(𝑅 ~RL (RLReg‘𝑅))〈(0g‘𝑅), (1r‘𝑅)〉) | 
| 78 | 16, 61, 40, 6, 17, 37, 77 | erldi 33267 | . . . . . . 7
⊢ ((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) → ∃𝑡 ∈ (RLReg‘𝑅)(𝑡(.r‘𝑅)(((1st
‘〈(1r‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(0g‘𝑅), (1r‘𝑅)〉))(-g‘𝑅)((1st
‘〈(0g‘𝑅), (1r‘𝑅)〉)(.r‘𝑅)(2nd
‘〈(1r‘𝑅), (1r‘𝑅)〉)))) = (0g‘𝑅)) | 
| 79 | 60, 78 | r19.29a 3161 | . . . . . 6
⊢ ((𝜑 ∧
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) →
(1r‘𝑅) =
(0g‘𝑅)) | 
| 80 | 8, 79 | mteqand 3032 | . . . . 5
⊢ (𝜑 →
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) ≠
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 81 |  | eqid 2736 | . . . . . 6
⊢ (𝑅 RLocal (RLReg‘𝑅)) = (𝑅 RLocal (RLReg‘𝑅)) | 
| 82 |  | eqid 2736 | . . . . . 6
⊢
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) | 
| 83 | 6, 5, 81, 61, 63, 71, 82 | rloc1r 33277 | . . . . 5
⊢ (𝜑 →
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) = (1r‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 84 |  | eqid 2736 | . . . . . 6
⊢
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) | 
| 85 | 6, 5, 81, 61, 63, 71, 84 | rloc0g 33276 | . . . . 5
⊢ (𝜑 →
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) = (0g‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 86 | 80, 83, 85 | 3netr3d 3016 | . . . 4
⊢ (𝜑 →
(1r‘(𝑅
RLocal (RLReg‘𝑅)))
≠ (0g‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 87 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑦 = [〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅)) → (𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑦) = (𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))[〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅)))) | 
| 88 | 87 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑦 = [〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅)) → ((𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑦) = (1r‘(𝑅 RLocal (RLReg‘𝑅))) ↔ (𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))[〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))) =
(1r‘(𝑅
RLocal (RLReg‘𝑅))))) | 
| 89 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑦 = [〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅)) → (𝑦(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥)) | 
| 90 | 89 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑦 = [〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅)) → ((𝑦(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅))) ↔ ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅))))) | 
| 91 | 88, 90 | anbi12d 632 | . . . . . . 7
⊢ (𝑦 = [〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅)) → (((𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑦) = (1r‘(𝑅 RLocal (RLReg‘𝑅))) ∧ (𝑦(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅)))) ↔ ((𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))[〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))) =
(1r‘(𝑅
RLocal (RLReg‘𝑅)))
∧ ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅)))))) | 
| 92 |  | simplr 768 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑏 ∈ (RLReg‘𝑅)) | 
| 93 | 39, 92 | sselid 3980 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑏 ∈ (Base‘𝑅)) | 
| 94 |  | simpllr 775 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑎 ∈ (Base‘𝑅)) | 
| 95 |  | simplr 768 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 96 | 72 | ad5antr 734 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → (𝑅 ~RL (RLReg‘𝑅)) Er ((Base‘𝑅) × (RLReg‘𝑅))) | 
| 97 | 18 | ad5antr 734 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 𝑅 ∈ Ring) | 
| 98 | 97, 20 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 99 | 16, 17, 6, 97, 98 | ringlzd 20293 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (0g‘𝑅)) | 
| 100 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 𝑎 = (0g‘𝑅)) | 
| 101 | 100 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → (𝑎(.r‘𝑅)(1r‘𝑅)) = ((0g‘𝑅)(.r‘𝑅)(1r‘𝑅))) | 
| 102 | 93 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 𝑏 ∈ (Base‘𝑅)) | 
| 103 | 16, 17, 6, 97, 102 | ringlzd 20293 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)𝑏) = (0g‘𝑅)) | 
| 104 | 99, 101, 103 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → (𝑎(.r‘𝑅)(1r‘𝑅)) = ((0g‘𝑅)(.r‘𝑅)𝑏)) | 
| 105 | 63 | ad5antr 734 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 𝑅 ∈ CRing) | 
| 106 | 94 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 𝑎 ∈ (Base‘𝑅)) | 
| 107 | 31 | ad5antr 734 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → (0g‘𝑅) ∈ (Base‘𝑅)) | 
| 108 | 92 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 𝑏 ∈ (RLReg‘𝑅)) | 
| 109 | 74 | ad5antr 734 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → (1r‘𝑅) ∈ (RLReg‘𝑅)) | 
| 110 | 16, 17, 61, 105, 106, 107, 108, 109 | fracerl 33309 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → (〈𝑎, 𝑏〉(𝑅 ~RL (RLReg‘𝑅))〈(0g‘𝑅), (1r‘𝑅)〉 ↔ (𝑎(.r‘𝑅)(1r‘𝑅)) = ((0g‘𝑅)(.r‘𝑅)𝑏))) | 
| 111 | 104, 110 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 〈𝑎, 𝑏〉(𝑅 ~RL (RLReg‘𝑅))〈(0g‘𝑅), (1r‘𝑅)〉) | 
| 112 | 96, 111 | erthi 8799 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 113 | 85 | ad5antr 734 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → [〈(0g‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) = (0g‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 114 | 95, 112, 113 | 3eqtrd 2780 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 𝑥 = (0g‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 115 |  | eldifsni 4789 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))})
→ 𝑥 ≠
(0g‘(𝑅
RLocal (RLReg‘𝑅)))) | 
| 116 | 115 | ad5antlr 735 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → 𝑥 ≠ (0g‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 117 | 116 | neneqd 2944 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ 𝑎 = (0g‘𝑅)) → ¬ 𝑥 = (0g‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 118 | 114, 117 | pm2.65da 816 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ¬ 𝑎 = (0g‘𝑅)) | 
| 119 | 118 | neqned 2946 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑎 ≠ (0g‘𝑅)) | 
| 120 | 94, 119 | eldifsnd 4786 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑎 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) | 
| 121 | 66 | ad4antr 732 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ((Base‘𝑅) ∖
{(0g‘𝑅)})
= (RLReg‘𝑅)) | 
| 122 | 120, 121 | eleqtrd 2842 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑎 ∈ (RLReg‘𝑅)) | 
| 123 | 93, 122 | opelxpd 5723 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 〈𝑏, 𝑎〉 ∈ ((Base‘𝑅) × (RLReg‘𝑅))) | 
| 124 |  | ovex 7465 | . . . . . . . . . 10
⊢ (𝑅 ~RL
(RLReg‘𝑅)) ∈
V | 
| 125 | 124 | ecelqsi 8814 | . . . . . . . . 9
⊢
(〈𝑏, 𝑎〉 ∈ ((Base‘𝑅) × (RLReg‘𝑅)) → [〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅)) ∈ (((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅)))) | 
| 126 | 123, 125 | syl 17 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → [〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅)) ∈ (((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅)))) | 
| 127 | 39 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → (RLReg‘𝑅) ⊆ (Base‘𝑅)) | 
| 128 | 16, 6, 17, 37, 62, 81, 61, 2, 127 | rlocbas 33272 | . . . . . . . . 9
⊢ (𝜑 → (((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅))) = (Base‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 129 | 128 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅))) = (Base‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 130 | 126, 129 | eleqtrd 2842 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → [〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅)) ∈ (Base‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 131 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘(𝑅
RLocal (RLReg‘𝑅))) =
(Base‘(𝑅 RLocal
(RLReg‘𝑅))) | 
| 132 |  | eqid 2736 | . . . . . . . . . 10
⊢
(.r‘(𝑅 RLocal (RLReg‘𝑅))) = (.r‘(𝑅 RLocal (RLReg‘𝑅))) | 
| 133 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 134 | 16, 17, 133, 81, 61, 63, 71 | rloccring 33275 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑅 RLocal (RLReg‘𝑅)) ∈ CRing) | 
| 135 | 134 | ad4antr 732 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑅 RLocal (RLReg‘𝑅)) ∈ CRing) | 
| 136 |  | simp-4r 783 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖ {(0g‘(𝑅 RLocal (RLReg‘𝑅)))})) | 
| 137 | 136 | eldifad 3962 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑥 ∈ (Base‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 138 | 131, 132,
135, 137, 130 | crngcomd 20253 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))[〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))) = ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥)) | 
| 139 |  | simpr 484 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 140 | 139 | oveq2d 7448 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))[〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅)))) | 
| 141 | 63 | ad4antr 732 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑅 ∈ CRing) | 
| 142 | 71 | ad4antr 732 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (RLReg‘𝑅) ∈
(SubMnd‘(mulGrp‘𝑅))) | 
| 143 | 16, 17, 133, 81, 61, 141, 142, 93, 94, 122, 92, 132 | rlocmulval 33274 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))[〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) = [〈(𝑏(.r‘𝑅)𝑎), (𝑎(.r‘𝑅)𝑏)〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 144 | 72 | ad4antr 732 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑅 ~RL (RLReg‘𝑅)) Er ((Base‘𝑅) × (RLReg‘𝑅))) | 
| 145 | 16, 17, 141, 93, 94 | crngcomd 20253 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑏(.r‘𝑅)𝑎) = (𝑎(.r‘𝑅)𝑏)) | 
| 146 | 18 | ad4antr 732 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 𝑅 ∈ Ring) | 
| 147 | 16, 17, 146, 93, 94 | ringcld 20258 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑏(.r‘𝑅)𝑎) ∈ (Base‘𝑅)) | 
| 148 | 16, 17, 5, 146, 147 | ringridmd 20271 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ((𝑏(.r‘𝑅)𝑎)(.r‘𝑅)(1r‘𝑅)) = (𝑏(.r‘𝑅)𝑎)) | 
| 149 | 16, 17, 146, 94, 93 | ringcld 20258 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑎(.r‘𝑅)𝑏) ∈ (Base‘𝑅)) | 
| 150 | 16, 17, 5, 146, 149 | ringlidmd 20270 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) →
((1r‘𝑅)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)) = (𝑎(.r‘𝑅)𝑏)) | 
| 151 | 145, 148,
150 | 3eqtr4d 2786 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ((𝑏(.r‘𝑅)𝑎)(.r‘𝑅)(1r‘𝑅)) = ((1r‘𝑅)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏))) | 
| 152 | 73 | ad4antr 732 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) →
(1r‘𝑅)
∈ (Base‘𝑅)) | 
| 153 | 94 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → 𝑎 ∈ (Base‘𝑅)) | 
| 154 | 31 | ad5antr 734 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → (0g‘𝑅) ∈ (Base‘𝑅)) | 
| 155 | 92 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → 𝑏 ∈ (RLReg‘𝑅)) | 
| 156 | 66 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → ((Base‘𝑅) ∖ {(0g‘𝑅)}) = (RLReg‘𝑅)) | 
| 157 | 155, 156 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → 𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) | 
| 158 | 2 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖ {(0g‘(𝑅 RLocal (RLReg‘𝑅)))})) → 𝑅 ∈ IDomn) | 
| 159 | 158 | ad4antr 732 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → 𝑅 ∈ IDomn) | 
| 160 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) | 
| 161 | 146 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → 𝑅 ∈ Ring) | 
| 162 | 93 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → 𝑏 ∈ (Base‘𝑅)) | 
| 163 | 16, 17, 6, 161, 162 | ringlzd 20293 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)𝑏) = (0g‘𝑅)) | 
| 164 | 160, 163 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → (𝑎(.r‘𝑅)𝑏) = ((0g‘𝑅)(.r‘𝑅)𝑏)) | 
| 165 | 16, 6, 17, 153, 154, 157, 159, 164 | idomrcan 33283 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) → 𝑎 = (0g‘𝑅)) | 
| 166 | 118, 165 | mtand 815 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ¬ (𝑎(.r‘𝑅)𝑏) = (0g‘𝑅)) | 
| 167 | 166 | neqned 2946 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑎(.r‘𝑅)𝑏) ≠ (0g‘𝑅)) | 
| 168 | 149, 167 | eldifsnd 4786 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑎(.r‘𝑅)𝑏) ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) | 
| 169 | 168, 121 | eleqtrd 2842 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑎(.r‘𝑅)𝑏) ∈ (RLReg‘𝑅)) | 
| 170 | 74 | ad4antr 732 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) →
(1r‘𝑅)
∈ (RLReg‘𝑅)) | 
| 171 | 16, 17, 61, 141, 147, 152, 169, 170 | fracerl 33309 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (〈(𝑏(.r‘𝑅)𝑎), (𝑎(.r‘𝑅)𝑏)〉(𝑅 ~RL (RLReg‘𝑅))〈(1r‘𝑅), (1r‘𝑅)〉 ↔ ((𝑏(.r‘𝑅)𝑎)(.r‘𝑅)(1r‘𝑅)) = ((1r‘𝑅)(.r‘𝑅)(𝑎(.r‘𝑅)𝑏)))) | 
| 172 | 151, 171 | mpbird 257 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → 〈(𝑏(.r‘𝑅)𝑎), (𝑎(.r‘𝑅)𝑏)〉(𝑅 ~RL (RLReg‘𝑅))〈(1r‘𝑅), (1r‘𝑅)〉) | 
| 173 | 144, 172 | erthi 8799 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → [〈(𝑏(.r‘𝑅)𝑎), (𝑎(.r‘𝑅)𝑏)〉](𝑅 ~RL (RLReg‘𝑅)) =
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 174 | 143, 173 | eqtrd 2776 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))[〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) =
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 175 | 83 | ad4antr 732 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) →
[〈(1r‘𝑅), (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) = (1r‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 176 | 140, 174,
175 | 3eqtrd 2780 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅)))) | 
| 177 | 138, 176 | eqtrd 2776 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))[〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))) =
(1r‘(𝑅
RLocal (RLReg‘𝑅)))) | 
| 178 | 177, 176 | jca 511 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ((𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))[〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))) =
(1r‘(𝑅
RLocal (RLReg‘𝑅)))
∧ ([〈𝑏, 𝑎〉](𝑅 ~RL (RLReg‘𝑅))(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅))))) | 
| 179 | 91, 130, 178 | rspcedvdw 3624 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))
∧ 𝑎 ∈
(Base‘𝑅)) ∧ 𝑏 ∈ (RLReg‘𝑅)) ∧ 𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) → ∃𝑦 ∈ (Base‘(𝑅 RLocal (RLReg‘𝑅)))((𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑦) = (1r‘(𝑅 RLocal (RLReg‘𝑅))) ∧ (𝑦(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅))))) | 
| 180 | 128 | difeq1d 4124 | . . . . . . . . . 10
⊢ (𝜑 → ((((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))})
= ((Base‘(𝑅 RLocal
(RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))})) | 
| 181 | 180 | eleq2d 2826 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ((((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))})
↔ 𝑥 ∈
((Base‘(𝑅 RLocal
(RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))}))) | 
| 182 | 181 | biimpar 477 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖ {(0g‘(𝑅 RLocal (RLReg‘𝑅)))})) → 𝑥 ∈ ((((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅))) ∖
{(0g‘(𝑅
RLocal (RLReg‘𝑅)))})) | 
| 183 | 182 | eldifad 3962 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖ {(0g‘(𝑅 RLocal (RLReg‘𝑅)))})) → 𝑥 ∈ (((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅)))) | 
| 184 | 183 | elrlocbasi 33271 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖ {(0g‘(𝑅 RLocal (RLReg‘𝑅)))})) → ∃𝑎 ∈ (Base‘𝑅)∃𝑏 ∈ (RLReg‘𝑅)𝑥 = [〈𝑎, 𝑏〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 185 | 179, 184 | r19.29vva 3215 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖ {(0g‘(𝑅 RLocal (RLReg‘𝑅)))})) → ∃𝑦 ∈ (Base‘(𝑅 RLocal (RLReg‘𝑅)))((𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑦) = (1r‘(𝑅 RLocal (RLReg‘𝑅))) ∧ (𝑦(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅))))) | 
| 186 | 185 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖ {(0g‘(𝑅 RLocal (RLReg‘𝑅)))})∃𝑦 ∈ (Base‘(𝑅 RLocal (RLReg‘𝑅)))((𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑦) = (1r‘(𝑅 RLocal (RLReg‘𝑅))) ∧ (𝑦(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅))))) | 
| 187 |  | eqid 2736 | . . . . 5
⊢
(0g‘(𝑅 RLocal (RLReg‘𝑅))) = (0g‘(𝑅 RLocal (RLReg‘𝑅))) | 
| 188 |  | eqid 2736 | . . . . 5
⊢
(1r‘(𝑅 RLocal (RLReg‘𝑅))) = (1r‘(𝑅 RLocal (RLReg‘𝑅))) | 
| 189 |  | eqid 2736 | . . . . 5
⊢
(Unit‘(𝑅
RLocal (RLReg‘𝑅))) =
(Unit‘(𝑅 RLocal
(RLReg‘𝑅))) | 
| 190 | 134 | crngringd 20244 | . . . . 5
⊢ (𝜑 → (𝑅 RLocal (RLReg‘𝑅)) ∈ Ring) | 
| 191 | 131, 187,
188, 132, 189, 190 | isdrng4 33299 | . . . 4
⊢ (𝜑 → ((𝑅 RLocal (RLReg‘𝑅)) ∈ DivRing ↔
((1r‘(𝑅
RLocal (RLReg‘𝑅)))
≠ (0g‘(𝑅 RLocal (RLReg‘𝑅))) ∧ ∀𝑥 ∈ ((Base‘(𝑅 RLocal (RLReg‘𝑅))) ∖ {(0g‘(𝑅 RLocal (RLReg‘𝑅)))})∃𝑦 ∈ (Base‘(𝑅 RLocal (RLReg‘𝑅)))((𝑥(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑦) = (1r‘(𝑅 RLocal (RLReg‘𝑅))) ∧ (𝑦(.r‘(𝑅 RLocal (RLReg‘𝑅)))𝑥) = (1r‘(𝑅 RLocal (RLReg‘𝑅))))))) | 
| 192 | 86, 186, 191 | mpbir2and 713 | . . 3
⊢ (𝜑 → (𝑅 RLocal (RLReg‘𝑅)) ∈ DivRing) | 
| 193 |  | isfld 20741 | . . 3
⊢ ((𝑅 RLocal (RLReg‘𝑅)) ∈ Field ↔ ((𝑅 RLocal (RLReg‘𝑅)) ∈ DivRing ∧ (𝑅 RLocal (RLReg‘𝑅)) ∈
CRing)) | 
| 194 | 192, 134,
193 | sylanbrc 583 | . 2
⊢ (𝜑 → (𝑅 RLocal (RLReg‘𝑅)) ∈ Field) | 
| 195 | 1, 194 | eqeltrid 2844 | 1
⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field) |