Proof of Theorem rrx2linest2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rrx2linest2.i | . . 3
⊢ 𝐼 = {1, 2} | 
| 2 |  | rrx2linest2.e | . . 3
⊢ 𝐸 = (ℝ^‘𝐼) | 
| 3 |  | rrx2linest2.p | . . 3
⊢ 𝑃 = (ℝ ↑m
𝐼) | 
| 4 |  | rrx2linest2.l | . . 3
⊢ 𝐿 = (LineM‘𝐸) | 
| 5 |  | rrx2linest2.b | . . 3
⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) | 
| 6 |  | eqid 2737 | . . 3
⊢ ((𝑌‘2) − (𝑋‘2)) = ((𝑌‘2) − (𝑋‘2)) | 
| 7 |  | rrx2linest2.c | . . 3
⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) | 
| 8 | 1, 2, 3, 4, 5, 6, 7 | rrx2linest 48663 | . 2
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶)}) | 
| 9 |  | eqcom 2744 | . . . 4
⊢ ((𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) ↔ ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) = (𝐵 · (𝑝‘2))) | 
| 10 | 1, 3 | rrx2pyel 48633 | . . . . . . . . . . 11
⊢ (𝑌 ∈ 𝑃 → (𝑌‘2) ∈ ℝ) | 
| 11 | 10 | 3ad2ant2 1135 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑌‘2) ∈ ℝ) | 
| 12 | 1, 3 | rrx2pyel 48633 | . . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) | 
| 13 | 12 | 3ad2ant1 1134 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋‘2) ∈ ℝ) | 
| 14 | 11, 13 | resubcld 11691 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑌‘2) − (𝑋‘2)) ∈ ℝ) | 
| 15 | 14 | adantr 480 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘2) − (𝑋‘2)) ∈ ℝ) | 
| 16 | 1, 3 | rrx2pxel 48632 | . . . . . . . . 9
⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ) | 
| 17 | 16 | adantl 481 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℝ) | 
| 18 | 15, 17 | remulcld 11291 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) ∈ ℝ) | 
| 19 | 18 | recnd 11289 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) ∈ ℂ) | 
| 20 | 1, 3 | rrx2pxel 48632 | . . . . . . . . . . . 12
⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ) | 
| 21 | 20 | 3ad2ant2 1135 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑌‘1) ∈ ℝ) | 
| 22 | 13, 21 | remulcld 11291 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑋‘2) · (𝑌‘1)) ∈ ℝ) | 
| 23 | 1, 3 | rrx2pxel 48632 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ) | 
| 24 | 23 | 3ad2ant1 1134 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋‘1) ∈ ℝ) | 
| 25 | 24, 11 | remulcld 11291 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑋‘1) · (𝑌‘2)) ∈ ℝ) | 
| 26 | 22, 25 | resubcld 11691 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ∈ ℝ) | 
| 27 | 7, 26 | eqeltrid 2845 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐶 ∈ ℝ) | 
| 28 | 27 | adantr 480 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℝ) | 
| 29 | 28 | recnd 11289 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ) | 
| 30 | 21, 24 | resubcld 11691 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑌‘1) − (𝑋‘1)) ∈ ℝ) | 
| 31 | 5, 30 | eqeltrid 2845 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐵 ∈ ℝ) | 
| 32 | 31 | adantr 480 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℝ) | 
| 33 | 1, 3 | rrx2pyel 48633 | . . . . . . . . 9
⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ) | 
| 34 | 33 | adantl 481 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℝ) | 
| 35 | 32, 34 | remulcld 11291 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℝ) | 
| 36 | 35 | recnd 11289 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℂ) | 
| 37 | 19, 29, 36 | addrsub 11680 | . . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) = (𝐵 · (𝑝‘2)) ↔ 𝐶 = ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))))) | 
| 38 |  | eqcom 2744 | . . . . . 6
⊢ (𝐶 = ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) ↔ ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) = 𝐶) | 
| 39 |  | rrx2linest2.a | . . . . . . . . . . . . 13
⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) | 
| 40 | 13, 11 | resubcld 11691 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑋‘2) − (𝑌‘2)) ∈ ℝ) | 
| 41 | 39, 40 | eqeltrid 2845 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐴 ∈ ℝ) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℝ) | 
| 43 | 42, 17 | remulcld 11291 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℝ) | 
| 44 | 43 | recnd 11289 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℂ) | 
| 45 | 44, 36 | addcomd 11463 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐵 · (𝑝‘2)) + (𝐴 · (𝑝‘1)))) | 
| 46 | 11 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝑌‘2) ∈ ℝ) | 
| 47 | 46 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝑌‘2) ∈ ℂ) | 
| 48 | 13 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝑋‘2) ∈ ℝ) | 
| 49 | 48 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝑋‘2) ∈ ℂ) | 
| 50 | 47, 49 | negsubdi2d 11636 | . . . . . . . . . . . 12
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → -((𝑌‘2) − (𝑋‘2)) = ((𝑋‘2) − (𝑌‘2))) | 
| 51 | 39, 50 | eqtr4id 2796 | . . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → 𝐴 = -((𝑌‘2) − (𝑋‘2))) | 
| 52 | 51 | oveq1d 7446 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = (-((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) | 
| 53 | 15 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘2) − (𝑋‘2)) ∈ ℂ) | 
| 54 | 17 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℂ) | 
| 55 | 53, 54 | mulneg1d 11716 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (-((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) = -(((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) | 
| 56 | 52, 55 | eqtrd 2777 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = -(((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) | 
| 57 | 56 | oveq2d 7447 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) + (𝐴 · (𝑝‘1))) = ((𝐵 · (𝑝‘2)) + -(((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)))) | 
| 58 | 36, 19 | negsubd 11626 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) + -(((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) = ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)))) | 
| 59 | 45, 57, 58 | 3eqtrd 2781 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)))) | 
| 60 | 59 | eqeq1d 2739 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) = 𝐶)) | 
| 61 | 38, 60 | bitr4id 290 | . . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (𝐶 = ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) ↔ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶)) | 
| 62 | 37, 61 | bitrd 279 | . . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) = (𝐵 · (𝑝‘2)) ↔ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶)) | 
| 63 | 9, 62 | bitrid 283 | . . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) ↔ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶)) | 
| 64 | 63 | rabbidva 3443 | . 2
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → {𝑝 ∈ 𝑃 ∣ (𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶)} = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) | 
| 65 | 8, 64 | eqtrd 2777 | 1
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) |