| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ltrelsr 11109 | . . . 4
⊢ 
<R ⊆ (R ×
R) | 
| 2 | 1 | brel 5749 | . . 3
⊢
(0R <R 𝐴 →
(0R ∈ R ∧ 𝐴 ∈ R)) | 
| 3 | 2 | simprd 495 | . 2
⊢
(0R <R 𝐴 → 𝐴 ∈ R) | 
| 4 |  | df-nr 11097 | . . 3
⊢
R = ((P × P) /
~R ) | 
| 5 |  | breq2 5146 | . . . 4
⊢
([〈𝑦, 𝑧〉]
~R = 𝐴 → (0R
<R [〈𝑦, 𝑧〉] ~R ↔
0R <R 𝐴)) | 
| 6 |  | oveq1 7439 | . . . . . 6
⊢
([〈𝑦, 𝑧〉]
~R = 𝐴 → ([〈𝑦, 𝑧〉] ~R
·R 𝑥) = (𝐴 ·R 𝑥)) | 
| 7 | 6 | eqeq1d 2738 | . . . . 5
⊢
([〈𝑦, 𝑧〉]
~R = 𝐴 → (([〈𝑦, 𝑧〉] ~R
·R 𝑥) = 1R ↔ (𝐴
·R 𝑥) =
1R)) | 
| 8 | 7 | rexbidv 3178 | . . . 4
⊢
([〈𝑦, 𝑧〉]
~R = 𝐴 → (∃𝑥 ∈ R ([〈𝑦, 𝑧〉] ~R
·R 𝑥) = 1R ↔
∃𝑥 ∈
R (𝐴
·R 𝑥) =
1R)) | 
| 9 | 5, 8 | imbi12d 344 | . . 3
⊢
([〈𝑦, 𝑧〉]
~R = 𝐴 → ((0R
<R [〈𝑦, 𝑧〉] ~R →
∃𝑥 ∈
R ([〈𝑦,
𝑧〉]
~R ·R 𝑥) = 1R)
↔ (0R <R 𝐴 → ∃𝑥 ∈ R (𝐴
·R 𝑥) =
1R))) | 
| 10 |  | gt0srpr 11119 | . . . . 5
⊢
(0R <R [〈𝑦, 𝑧〉] ~R ↔
𝑧<P 𝑦) | 
| 11 |  | ltexpri 11084 | . . . . 5
⊢ (𝑧<P
𝑦 → ∃𝑤 ∈ P (𝑧 +P
𝑤) = 𝑦) | 
| 12 | 10, 11 | sylbi 217 | . . . 4
⊢
(0R <R [〈𝑦, 𝑧〉] ~R →
∃𝑤 ∈
P (𝑧
+P 𝑤) = 𝑦) | 
| 13 |  | recexpr 11092 | . . . . . 6
⊢ (𝑤 ∈ P →
∃𝑣 ∈
P (𝑤
·P 𝑣) =
1P) | 
| 14 |  | 1pr 11056 | . . . . . . . . . . . 12
⊢
1P ∈ P | 
| 15 |  | addclpr 11059 | . . . . . . . . . . . 12
⊢ ((𝑣 ∈ P ∧
1P ∈ P) → (𝑣 +P
1P) ∈ P) | 
| 16 | 14, 15 | mpan2 691 | . . . . . . . . . . 11
⊢ (𝑣 ∈ P →
(𝑣
+P 1P) ∈
P) | 
| 17 |  | enrex 11108 | . . . . . . . . . . . 12
⊢ 
~R ∈ V | 
| 18 | 17, 4 | ecopqsi 8815 | . . . . . . . . . . 11
⊢ (((𝑣 +P
1P) ∈ P ∧
1P ∈ P) → [〈(𝑣 +P
1P), 1P〉]
~R ∈ R) | 
| 19 | 16, 14, 18 | sylancl 586 | . . . . . . . . . 10
⊢ (𝑣 ∈ P →
[〈(𝑣
+P 1P),
1P〉] ~R ∈
R) | 
| 20 | 19 | ad2antlr 727 | . . . . . . . . 9
⊢ ((((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) ∧ ((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦)) → [〈(𝑣 +P
1P), 1P〉]
~R ∈ R) | 
| 21 | 16, 14 | jctir 520 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ P →
((𝑣
+P 1P) ∈ P
∧ 1P ∈ P)) | 
| 22 | 21 | anim2i 617 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) → ((𝑦
∈ P ∧ 𝑧 ∈ P) ∧ ((𝑣 +P
1P) ∈ P ∧
1P ∈ P))) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) ∧ ((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦)) → ((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧
((𝑣
+P 1P) ∈ P
∧ 1P ∈ P))) | 
| 24 |  | mulsrpr 11117 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ ((𝑣
+P 1P) ∈ P
∧ 1P ∈ P)) → ([〈𝑦, 𝑧〉] ~R
·R [〈(𝑣 +P
1P), 1P〉]
~R ) = [〈((𝑦 ·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)), ((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P)))〉] ~R
) | 
| 25 | 23, 24 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) ∧ ((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦)) → ([〈𝑦, 𝑧〉] ~R
·R [〈(𝑣 +P
1P), 1P〉]
~R ) = [〈((𝑦 ·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)), ((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P)))〉] ~R
) | 
| 26 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 +P
𝑤) = 𝑦 → ((𝑧 +P 𝑤)
·P 𝑣) = (𝑦 ·P 𝑣)) | 
| 27 | 26 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 +P
𝑤) = 𝑦 → (𝑦 ·P 𝑣) = ((𝑧 +P 𝑤)
·P 𝑣)) | 
| 28 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑧 ∈ V | 
| 29 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑤 ∈ V | 
| 30 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑣 ∈ V | 
| 31 |  | mulcompr 11064 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢
·P 𝑓) = (𝑓 ·P 𝑢) | 
| 32 |  | distrpr 11069 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢
·P (𝑓 +P 𝑥)) = ((𝑢 ·P 𝑓) +P
(𝑢
·P 𝑥)) | 
| 33 | 28, 29, 30, 31, 32 | caovdir 7668 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 +P
𝑤)
·P 𝑣) = ((𝑧 ·P 𝑣) +P
(𝑤
·P 𝑣)) | 
| 34 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤
·P 𝑣) = 1P →
((𝑧
·P 𝑣) +P (𝑤
·P 𝑣)) = ((𝑧 ·P 𝑣) +P
1P)) | 
| 35 | 33, 34 | eqtrid 2788 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤
·P 𝑣) = 1P →
((𝑧
+P 𝑤) ·P 𝑣) = ((𝑧 ·P 𝑣) +P
1P)) | 
| 36 | 27, 35 | sylan9eqr 2798 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦) → (𝑦 ·P 𝑣) = ((𝑧 ·P 𝑣) +P
1P)) | 
| 37 | 36 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦) → ((𝑦 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) = (((𝑧 ·P 𝑣) +P
1P) +P ((𝑦 ·P
1P) +P (𝑧 ·P
1P)))) | 
| 38 |  | ovex 7465 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧
·P 𝑣) ∈ V | 
| 39 | 14 | elexi 3502 | . . . . . . . . . . . . . . . . . 18
⊢
1P ∈ V | 
| 40 |  | ovex 7465 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦
·P 1P)
+P (𝑧 ·P
1P)) ∈ V | 
| 41 |  | addcompr 11062 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 +P
𝑓) = (𝑓 +P 𝑢) | 
| 42 |  | addasspr 11063 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 +P
𝑓)
+P 𝑥) = (𝑢 +P (𝑓 +P
𝑥)) | 
| 43 | 38, 39, 40, 41, 42 | caov32 7661 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑧
·P 𝑣) +P
1P) +P ((𝑦 ·P
1P) +P (𝑧 ·P
1P))) = (((𝑧 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
1P) | 
| 44 | 37, 43 | eqtrdi 2792 | . . . . . . . . . . . . . . . 16
⊢ (((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦) → ((𝑦 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) = (((𝑧 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
1P)) | 
| 45 | 44 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦) → (((𝑦 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
1P) = ((((𝑧 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
1P) +P
1P)) | 
| 46 |  | addasspr 11063 | . . . . . . . . . . . . . . 15
⊢ ((((𝑧
·P 𝑣) +P ((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
1P) +P
1P) = (((𝑧 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
(1P +P
1P)) | 
| 47 | 45, 46 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦) → (((𝑦 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
1P) = (((𝑧 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
(1P +P
1P))) | 
| 48 |  | distrpr 11069 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦
·P (𝑣 +P
1P)) = ((𝑦 ·P 𝑣) +P
(𝑦
·P
1P)) | 
| 49 | 48 | oveq1i 7442 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦
·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) = (((𝑦 ·P 𝑣) +P
(𝑦
·P 1P))
+P (𝑧 ·P
1P)) | 
| 50 |  | addasspr 11063 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦
·P 𝑣) +P (𝑦
·P 1P))
+P (𝑧 ·P
1P)) = ((𝑦 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) | 
| 51 | 49, 50 | eqtri 2764 | . . . . . . . . . . . . . . 15
⊢ ((𝑦
·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) = ((𝑦 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) | 
| 52 | 51 | oveq1i 7442 | . . . . . . . . . . . . . 14
⊢ (((𝑦
·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) +P
1P) = (((𝑦 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
1P) | 
| 53 |  | distrpr 11069 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧
·P (𝑣 +P
1P)) = ((𝑧 ·P 𝑣) +P
(𝑧
·P
1P)) | 
| 54 | 53 | oveq2i 7443 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦
·P 1P)
+P (𝑧 ·P (𝑣 +P
1P))) = ((𝑦 ·P
1P) +P ((𝑧 ·P 𝑣) +P
(𝑧
·P
1P))) | 
| 55 |  | ovex 7465 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦
·P 1P) ∈
V | 
| 56 |  | ovex 7465 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧
·P 1P) ∈
V | 
| 57 | 55, 38, 56, 41, 42 | caov12 7662 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦
·P 1P)
+P ((𝑧 ·P 𝑣) +P
(𝑧
·P 1P))) = ((𝑧
·P 𝑣) +P ((𝑦
·P 1P)
+P (𝑧 ·P
1P))) | 
| 58 | 54, 57 | eqtri 2764 | . . . . . . . . . . . . . . 15
⊢ ((𝑦
·P 1P)
+P (𝑧 ·P (𝑣 +P
1P))) = ((𝑧 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) | 
| 59 | 58 | oveq1i 7442 | . . . . . . . . . . . . . 14
⊢ (((𝑦
·P 1P)
+P (𝑧 ·P (𝑣 +P
1P))) +P
(1P +P
1P)) = (((𝑧 ·P 𝑣) +P
((𝑦
·P 1P)
+P (𝑧 ·P
1P))) +P
(1P +P
1P)) | 
| 60 | 47, 52, 59 | 3eqtr4g 2801 | . . . . . . . . . . . . 13
⊢ (((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦) → (((𝑦 ·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) +P
1P) = (((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P))) +P
(1P +P
1P))) | 
| 61 |  | mulclpr 11061 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ P ∧
(𝑣
+P 1P) ∈
P) → (𝑦
·P (𝑣 +P
1P)) ∈ P) | 
| 62 | 16, 61 | sylan2 593 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ P ∧
𝑣 ∈ P)
→ (𝑦
·P (𝑣 +P
1P)) ∈ P) | 
| 63 |  | mulclpr 11061 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ P ∧
1P ∈ P) → (𝑧 ·P
1P) ∈ P) | 
| 64 | 14, 63 | mpan2 691 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ P →
(𝑧
·P 1P) ∈
P) | 
| 65 |  | addclpr 11059 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦
·P (𝑣 +P
1P)) ∈ P ∧ (𝑧 ·P
1P) ∈ P) → ((𝑦
·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) ∈ P) | 
| 66 | 62, 64, 65 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ P ∧
𝑣 ∈ P)
∧ 𝑧 ∈
P) → ((𝑦
·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) ∈ P) | 
| 67 | 66 | an32s 652 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) → ((𝑦
·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) ∈ P) | 
| 68 |  | mulclpr 11061 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ P ∧
1P ∈ P) → (𝑦 ·P
1P) ∈ P) | 
| 69 | 14, 68 | mpan2 691 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ P →
(𝑦
·P 1P) ∈
P) | 
| 70 |  | mulclpr 11061 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ P ∧
(𝑣
+P 1P) ∈
P) → (𝑧
·P (𝑣 +P
1P)) ∈ P) | 
| 71 | 16, 70 | sylan2 593 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ P ∧
𝑣 ∈ P)
→ (𝑧
·P (𝑣 +P
1P)) ∈ P) | 
| 72 |  | addclpr 11059 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦
·P 1P) ∈
P ∧ (𝑧
·P (𝑣 +P
1P)) ∈ P) → ((𝑦
·P 1P)
+P (𝑧 ·P (𝑣 +P
1P))) ∈ P) | 
| 73 | 69, 71, 72 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ P ∧
(𝑧 ∈ P
∧ 𝑣 ∈
P)) → ((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P))) ∈ P) | 
| 74 | 73 | anassrs 467 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) → ((𝑦
·P 1P)
+P (𝑧 ·P (𝑣 +P
1P))) ∈ P) | 
| 75 | 67, 74 | jca 511 | . . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) → (((𝑦 ·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) ∈ P ∧ ((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P))) ∈ P)) | 
| 76 |  | addclpr 11059 | . . . . . . . . . . . . . . . 16
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P +P
1P) ∈ P) | 
| 77 | 14, 14, 76 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢
(1P +P
1P) ∈ P | 
| 78 | 77, 14 | pm3.2i 470 | . . . . . . . . . . . . . 14
⊢
((1P +P
1P) ∈ P ∧
1P ∈ P) | 
| 79 |  | enreceq 11107 | . . . . . . . . . . . . . 14
⊢
(((((𝑦
·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) ∈ P ∧ ((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P))) ∈ P) ∧
((1P +P
1P) ∈ P ∧
1P ∈ P)) → ([〈((𝑦
·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)), ((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P)))〉] ~R =
[〈(1P +P
1P), 1P〉]
~R ↔ (((𝑦 ·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) +P
1P) = (((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P))) +P
(1P +P
1P)))) | 
| 80 | 75, 78, 79 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) → ([〈((𝑦 ·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)), ((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P)))〉] ~R =
[〈(1P +P
1P), 1P〉]
~R ↔ (((𝑦 ·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)) +P
1P) = (((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P))) +P
(1P +P
1P)))) | 
| 81 | 60, 80 | imbitrrid 246 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) → (((𝑤 ·P 𝑣) = 1P
∧ (𝑧
+P 𝑤) = 𝑦) → [〈((𝑦 ·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)), ((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P)))〉] ~R =
[〈(1P +P
1P), 1P〉]
~R )) | 
| 82 | 81 | imp 406 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) ∧ ((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦)) → [〈((𝑦 ·P (𝑣 +P
1P)) +P (𝑧 ·P
1P)), ((𝑦 ·P
1P) +P (𝑧 ·P (𝑣 +P
1P)))〉] ~R =
[〈(1P +P
1P), 1P〉]
~R ) | 
| 83 | 25, 82 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) ∧ ((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦)) → ([〈𝑦, 𝑧〉] ~R
·R [〈(𝑣 +P
1P), 1P〉]
~R ) = [〈(1P
+P 1P),
1P〉] ~R
) | 
| 84 |  | df-1r 11102 | . . . . . . . . . 10
⊢
1R = [〈(1P
+P 1P),
1P〉] ~R | 
| 85 | 83, 84 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) ∧ ((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦)) → ([〈𝑦, 𝑧〉] ~R
·R [〈(𝑣 +P
1P), 1P〉]
~R ) = 1R) | 
| 86 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑥 = [〈(𝑣 +P
1P), 1P〉]
~R → ([〈𝑦, 𝑧〉] ~R
·R 𝑥) = ([〈𝑦, 𝑧〉] ~R
·R [〈(𝑣 +P
1P), 1P〉]
~R )) | 
| 87 | 86 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (𝑥 = [〈(𝑣 +P
1P), 1P〉]
~R → (([〈𝑦, 𝑧〉] ~R
·R 𝑥) = 1R ↔
([〈𝑦, 𝑧〉]
~R ·R [〈(𝑣 +P
1P), 1P〉]
~R ) = 1R)) | 
| 88 | 87 | rspcev 3621 | . . . . . . . . 9
⊢
(([〈(𝑣
+P 1P),
1P〉] ~R ∈
R ∧ ([〈𝑦, 𝑧〉] ~R
·R [〈(𝑣 +P
1P), 1P〉]
~R ) = 1R) →
∃𝑥 ∈
R ([〈𝑦,
𝑧〉]
~R ·R 𝑥) =
1R) | 
| 89 | 20, 85, 88 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝑦 ∈ P ∧
𝑧 ∈ P)
∧ 𝑣 ∈
P) ∧ ((𝑤
·P 𝑣) = 1P ∧ (𝑧 +P
𝑤) = 𝑦)) → ∃𝑥 ∈ R ([〈𝑦, 𝑧〉] ~R
·R 𝑥) =
1R) | 
| 90 | 89 | exp43 436 | . . . . . . 7
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (𝑣 ∈
P → ((𝑤
·P 𝑣) = 1P →
((𝑧
+P 𝑤) = 𝑦 → ∃𝑥 ∈ R ([〈𝑦, 𝑧〉] ~R
·R 𝑥) =
1R)))) | 
| 91 | 90 | rexlimdv 3152 | . . . . . 6
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (∃𝑣 ∈
P (𝑤
·P 𝑣) = 1P →
((𝑧
+P 𝑤) = 𝑦 → ∃𝑥 ∈ R ([〈𝑦, 𝑧〉] ~R
·R 𝑥) =
1R))) | 
| 92 | 13, 91 | syl5 34 | . . . . 5
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (𝑤 ∈
P → ((𝑧
+P 𝑤) = 𝑦 → ∃𝑥 ∈ R ([〈𝑦, 𝑧〉] ~R
·R 𝑥) =
1R))) | 
| 93 | 92 | rexlimdv 3152 | . . . 4
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (∃𝑤 ∈
P (𝑧
+P 𝑤) = 𝑦 → ∃𝑥 ∈ R ([〈𝑦, 𝑧〉] ~R
·R 𝑥) =
1R)) | 
| 94 | 12, 93 | syl5 34 | . . 3
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (0R <R [〈𝑦, 𝑧〉] ~R →
∃𝑥 ∈
R ([〈𝑦,
𝑧〉]
~R ·R 𝑥) =
1R)) | 
| 95 | 4, 9, 94 | ecoptocl 8848 | . 2
⊢ (𝐴 ∈ R →
(0R <R 𝐴 → ∃𝑥 ∈ R (𝐴 ·R 𝑥) =
1R)) | 
| 96 | 3, 95 | mpcom 38 | 1
⊢
(0R <R 𝐴 → ∃𝑥 ∈ R (𝐴
·R 𝑥) =
1R) |