Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  line2 Structured version   Visualization version   GIF version

Theorem line2 47600
Description: Example for a line 𝐺 passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023.)
Hypotheses
Ref Expression
line2.i 𝐼 = {1, 2}
line2.e 𝐸 = (ℝ^β€˜πΌ)
line2.p 𝑃 = (ℝ ↑m 𝐼)
line2.l 𝐿 = (LineMβ€˜πΈ)
line2.g 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) = 𝐢}
line2.x 𝑋 = {⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}
line2.y π‘Œ = {⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}
Assertion
Ref Expression
line2 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐺 = (π‘‹πΏπ‘Œ))
Distinct variable groups:   𝐴,𝑝   𝐡,𝑝   𝐢,𝑝   𝐸,𝑝   𝐼,𝑝   𝑃,𝑝   𝑋,𝑝   π‘Œ,𝑝
Allowed substitution hints:   𝐺(𝑝)   𝐿(𝑝)

Proof of Theorem line2
StepHypRef Expression
1 simp1 1135 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐴 ∈ ℝ)
21adantr 480 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ 𝐴 ∈ ℝ)
3 line2.i . . . . . . . . . . . . . 14 𝐼 = {1, 2}
4 line2.p . . . . . . . . . . . . . 14 𝑃 = (ℝ ↑m 𝐼)
53, 4rrx2pxel 47559 . . . . . . . . . . . . 13 (𝑝 ∈ 𝑃 β†’ (π‘β€˜1) ∈ ℝ)
65adantl 481 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (π‘β€˜1) ∈ ℝ)
72, 6remulcld 11251 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (𝐴 Β· (π‘β€˜1)) ∈ ℝ)
87recnd 11249 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (𝐴 Β· (π‘β€˜1)) ∈ β„‚)
9 simpl2l 1225 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ 𝐡 ∈ ℝ)
103, 4rrx2pyel 47560 . . . . . . . . . . . . 13 (𝑝 ∈ 𝑃 β†’ (π‘β€˜2) ∈ ℝ)
1110adantl 481 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (π‘β€˜2) ∈ ℝ)
129, 11remulcld 11251 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (𝐡 Β· (π‘β€˜2)) ∈ ℝ)
1312recnd 11249 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (𝐡 Β· (π‘β€˜2)) ∈ β„‚)
14 simpl 482 . . . . . . . . . . . . 13 ((𝐡 ∈ ℝ ∧ 𝐡 β‰  0) β†’ 𝐡 ∈ ℝ)
1514recnd 11249 . . . . . . . . . . . 12 ((𝐡 ∈ ℝ ∧ 𝐡 β‰  0) β†’ 𝐡 ∈ β„‚)
16153ad2ant2 1133 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐡 ∈ β„‚)
1716adantr 480 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ 𝐡 ∈ β„‚)
18 simp2r 1199 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐡 β‰  0)
1918adantr 480 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ 𝐡 β‰  0)
208, 13, 17, 19divdird 12035 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) / 𝐡) = (((𝐴 Β· (π‘β€˜1)) / 𝐡) + ((𝐡 Β· (π‘β€˜2)) / 𝐡)))
2110recnd 11249 . . . . . . . . . . . 12 (𝑝 ∈ 𝑃 β†’ (π‘β€˜2) ∈ β„‚)
2221adantl 481 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (π‘β€˜2) ∈ β„‚)
2322, 17, 19divcan3d 12002 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((𝐡 Β· (π‘β€˜2)) / 𝐡) = (π‘β€˜2))
2423oveq2d 7428 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((𝐴 Β· (π‘β€˜1)) / 𝐡) + ((𝐡 Β· (π‘β€˜2)) / 𝐡)) = (((𝐴 Β· (π‘β€˜1)) / 𝐡) + (π‘β€˜2)))
2520, 24eqtrd 2771 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) / 𝐡) = (((𝐴 Β· (π‘β€˜1)) / 𝐡) + (π‘β€˜2)))
2625eqeq1d 2733 . . . . . . 7 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) / 𝐡) = (𝐢 / 𝐡) ↔ (((𝐴 Β· (π‘β€˜1)) / 𝐡) + (π‘β€˜2)) = (𝐢 / 𝐡)))
277, 9, 19redivcld 12049 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((𝐴 Β· (π‘β€˜1)) / 𝐡) ∈ ℝ)
2827recnd 11249 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((𝐴 Β· (π‘β€˜1)) / 𝐡) ∈ β„‚)
29 simp3 1137 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐢 ∈ ℝ)
30143ad2ant2 1133 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐡 ∈ ℝ)
3129, 30, 18redivcld 12049 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (𝐢 / 𝐡) ∈ ℝ)
3231recnd 11249 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (𝐢 / 𝐡) ∈ β„‚)
3332adantr 480 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (𝐢 / 𝐡) ∈ β„‚)
3428, 22, 33addrsub 11638 . . . . . . 7 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((((𝐴 Β· (π‘β€˜1)) / 𝐡) + (π‘β€˜2)) = (𝐢 / 𝐡) ↔ (π‘β€˜2) = ((𝐢 / 𝐡) βˆ’ ((𝐴 Β· (π‘β€˜1)) / 𝐡))))
35 simpl3 1192 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ 𝐢 ∈ ℝ)
3635, 9, 19redivcld 12049 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (𝐢 / 𝐡) ∈ ℝ)
3736recnd 11249 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (𝐢 / 𝐡) ∈ β„‚)
3828, 37negsubdi2d 11594 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ -(((𝐴 Β· (π‘β€˜1)) / 𝐡) βˆ’ (𝐢 / 𝐡)) = ((𝐢 / 𝐡) βˆ’ ((𝐴 Β· (π‘β€˜1)) / 𝐡)))
3928, 37negsubdid 11593 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ -(((𝐴 Β· (π‘β€˜1)) / 𝐡) βˆ’ (𝐢 / 𝐡)) = (-((𝐴 Β· (π‘β€˜1)) / 𝐡) + (𝐢 / 𝐡)))
4038, 39eqtr3d 2773 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((𝐢 / 𝐡) βˆ’ ((𝐴 Β· (π‘β€˜1)) / 𝐡)) = (-((𝐴 Β· (π‘β€˜1)) / 𝐡) + (𝐢 / 𝐡)))
4140eqeq2d 2742 . . . . . . 7 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((π‘β€˜2) = ((𝐢 / 𝐡) βˆ’ ((𝐴 Β· (π‘β€˜1)) / 𝐡)) ↔ (π‘β€˜2) = (-((𝐴 Β· (π‘β€˜1)) / 𝐡) + (𝐢 / 𝐡))))
4226, 34, 413bitrd 305 . . . . . 6 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) / 𝐡) = (𝐢 / 𝐡) ↔ (π‘β€˜2) = (-((𝐴 Β· (π‘β€˜1)) / 𝐡) + (𝐢 / 𝐡))))
437, 12readdcld 11250 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) ∈ ℝ)
4443recnd 11249 . . . . . . 7 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) ∈ β„‚)
4529recnd 11249 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐢 ∈ β„‚)
4645adantr 480 . . . . . . 7 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ 𝐢 ∈ β„‚)
47 recn 11206 . . . . . . . . . 10 (𝐡 ∈ ℝ β†’ 𝐡 ∈ β„‚)
4847anim1i 614 . . . . . . . . 9 ((𝐡 ∈ ℝ ∧ 𝐡 β‰  0) β†’ (𝐡 ∈ β„‚ ∧ 𝐡 β‰  0))
49483ad2ant2 1133 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (𝐡 ∈ β„‚ ∧ 𝐡 β‰  0))
5049adantr 480 . . . . . . 7 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (𝐡 ∈ β„‚ ∧ 𝐡 β‰  0))
51 div11 11907 . . . . . . 7 ((((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) ∈ β„‚ ∧ 𝐢 ∈ β„‚ ∧ (𝐡 ∈ β„‚ ∧ 𝐡 β‰  0)) β†’ ((((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) / 𝐡) = (𝐢 / 𝐡) ↔ ((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) = 𝐢))
5244, 46, 50, 51syl3anc 1370 . . . . . 6 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) / 𝐡) = (𝐢 / 𝐡) ↔ ((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) = 𝐢))
538, 17, 19divnegd 12010 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ -((𝐴 Β· (π‘β€˜1)) / 𝐡) = (-(𝐴 Β· (π‘β€˜1)) / 𝐡))
541recnd 11249 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐴 ∈ β„‚)
5554adantr 480 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ 𝐴 ∈ β„‚)
565recnd 11249 . . . . . . . . . . . . . 14 (𝑝 ∈ 𝑃 β†’ (π‘β€˜1) ∈ β„‚)
5756adantl 481 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (π‘β€˜1) ∈ β„‚)
5855, 57mulneg1d 11674 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (-𝐴 Β· (π‘β€˜1)) = -(𝐴 Β· (π‘β€˜1)))
5958eqcomd 2737 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ -(𝐴 Β· (π‘β€˜1)) = (-𝐴 Β· (π‘β€˜1)))
6059oveq1d 7427 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (-(𝐴 Β· (π‘β€˜1)) / 𝐡) = ((-𝐴 Β· (π‘β€˜1)) / 𝐡))
6153, 60eqtrd 2771 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ -((𝐴 Β· (π‘β€˜1)) / 𝐡) = ((-𝐴 Β· (π‘β€˜1)) / 𝐡))
62 renegcl 11530 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ β†’ -𝐴 ∈ ℝ)
6362recnd 11249 . . . . . . . . . . . 12 (𝐴 ∈ ℝ β†’ -𝐴 ∈ β„‚)
64633ad2ant1 1132 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ -𝐴 ∈ β„‚)
6564adantr 480 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ -𝐴 ∈ β„‚)
66 div23 11898 . . . . . . . . . 10 ((-𝐴 ∈ β„‚ ∧ (π‘β€˜1) ∈ β„‚ ∧ (𝐡 ∈ β„‚ ∧ 𝐡 β‰  0)) β†’ ((-𝐴 Β· (π‘β€˜1)) / 𝐡) = ((-𝐴 / 𝐡) Β· (π‘β€˜1)))
6765, 57, 50, 66syl3anc 1370 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((-𝐴 Β· (π‘β€˜1)) / 𝐡) = ((-𝐴 / 𝐡) Β· (π‘β€˜1)))
68 line2.x . . . . . . . . . . . . . . 15 𝑋 = {⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}
6968fveq1i 6892 . . . . . . . . . . . . . 14 (π‘‹β€˜1) = ({⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}β€˜1)
70 1ex 11217 . . . . . . . . . . . . . . . 16 1 ∈ V
71 c0ex 11215 . . . . . . . . . . . . . . . 16 0 ∈ V
72 1ne2 12427 . . . . . . . . . . . . . . . 16 1 β‰  2
7370, 71, 723pm3.2i 1338 . . . . . . . . . . . . . . 15 (1 ∈ V ∧ 0 ∈ V ∧ 1 β‰  2)
74 fvpr1g 7190 . . . . . . . . . . . . . . 15 ((1 ∈ V ∧ 0 ∈ V ∧ 1 β‰  2) β†’ ({⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}β€˜1) = 0)
7573, 74mp1i 13 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ ({⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}β€˜1) = 0)
7669, 75eqtrid 2783 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (π‘‹β€˜1) = 0)
7776adantr 480 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (π‘‹β€˜1) = 0)
7877oveq2d 7428 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((π‘β€˜1) βˆ’ (π‘‹β€˜1)) = ((π‘β€˜1) βˆ’ 0))
7957subid1d 11567 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((π‘β€˜1) βˆ’ 0) = (π‘β€˜1))
8078, 79eqtr2d 2772 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (π‘β€˜1) = ((π‘β€˜1) βˆ’ (π‘‹β€˜1)))
8180oveq2d 7428 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((-𝐴 / 𝐡) Β· (π‘β€˜1)) = ((-𝐴 / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))))
8261, 67, 813eqtrd 2775 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ -((𝐴 Β· (π‘β€˜1)) / 𝐡) = ((-𝐴 / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))))
8382oveq1d 7427 . . . . . . 7 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (-((𝐴 Β· (π‘β€˜1)) / 𝐡) + (𝐢 / 𝐡)) = (((-𝐴 / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)))
8483eqeq2d 2742 . . . . . 6 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((π‘β€˜2) = (-((𝐴 Β· (π‘β€˜1)) / 𝐡) + (𝐢 / 𝐡)) ↔ (π‘β€˜2) = (((-𝐴 / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡))))
8542, 52, 843bitr3d 309 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) = 𝐢 ↔ (π‘β€˜2) = (((-𝐴 / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡))))
86 recn 11206 . . . . . . . . . . . . 13 (𝐢 ∈ ℝ β†’ 𝐢 ∈ β„‚)
8786adantl 481 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ 𝐢 ∈ β„‚)
88 recn 11206 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ β†’ 𝐴 ∈ β„‚)
8988adantr 480 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ 𝐴 ∈ β„‚)
90 sub32 11501 . . . . . . . . . . . . 13 ((𝐢 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) = ((𝐢 βˆ’ 𝐢) βˆ’ 𝐴))
91 subid 11486 . . . . . . . . . . . . . . . 16 (𝐢 ∈ β„‚ β†’ (𝐢 βˆ’ 𝐢) = 0)
92913ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝐢 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ (𝐢 βˆ’ 𝐢) = 0)
9392oveq1d 7427 . . . . . . . . . . . . . 14 ((𝐢 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐢 βˆ’ 𝐢) βˆ’ 𝐴) = (0 βˆ’ 𝐴))
94 df-neg 11454 . . . . . . . . . . . . . 14 -𝐴 = (0 βˆ’ 𝐴)
9593, 94eqtr4di 2789 . . . . . . . . . . . . 13 ((𝐢 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ ((𝐢 βˆ’ 𝐢) βˆ’ 𝐴) = -𝐴)
9690, 95eqtr2d 2772 . . . . . . . . . . . 12 ((𝐢 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ -𝐴 = ((𝐢 βˆ’ 𝐴) βˆ’ 𝐢))
9787, 89, 87, 96syl3anc 1370 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ -𝐴 = ((𝐢 βˆ’ 𝐴) βˆ’ 𝐢))
98973adant2 1130 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ -𝐴 = ((𝐢 βˆ’ 𝐴) βˆ’ 𝐢))
9998oveq1d 7427 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (-𝐴 / 𝐡) = (((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡))
10099adantr 480 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (-𝐴 / 𝐡) = (((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡))
101100oveq1d 7427 . . . . . . 7 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((-𝐴 / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) = ((((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))))
102101oveq1d 7427 . . . . . 6 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((-𝐴 / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)) = (((((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)))
103102eqeq2d 2742 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((π‘β€˜2) = (((-𝐴 / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)) ↔ (π‘β€˜2) = (((((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡))))
10485, 103bitrd 279 . . . 4 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) = 𝐢 ↔ (π‘β€˜2) = (((((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡))))
105 line2.y . . . . . . . . . . 11 π‘Œ = {⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}
106105fveq1i 6892 . . . . . . . . . 10 (π‘Œβ€˜2) = ({⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}β€˜2)
107 2ex 12296 . . . . . . . . . . . . . 14 2 ∈ V
108107a1i 11 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 2 ∈ V)
109 resubcl 11531 . . . . . . . . . . . . . . . 16 ((𝐢 ∈ ℝ ∧ 𝐴 ∈ ℝ) β†’ (𝐢 βˆ’ 𝐴) ∈ ℝ)
110109ancoms 458 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐢 ∈ ℝ) β†’ (𝐢 βˆ’ 𝐴) ∈ ℝ)
1111103adant2 1130 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (𝐢 βˆ’ 𝐴) ∈ ℝ)
112111, 30, 18redivcld 12049 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ ((𝐢 βˆ’ 𝐴) / 𝐡) ∈ ℝ)
11372a1i 11 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 1 β‰  2)
114108, 112, 1133jca 1127 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (2 ∈ V ∧ ((𝐢 βˆ’ 𝐴) / 𝐡) ∈ ℝ ∧ 1 β‰  2))
115114adantr 480 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (2 ∈ V ∧ ((𝐢 βˆ’ 𝐴) / 𝐡) ∈ ℝ ∧ 1 β‰  2))
116 fvpr2g 7191 . . . . . . . . . . 11 ((2 ∈ V ∧ ((𝐢 βˆ’ 𝐴) / 𝐡) ∈ ℝ ∧ 1 β‰  2) β†’ ({⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}β€˜2) = ((𝐢 βˆ’ 𝐴) / 𝐡))
117115, 116syl 17 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ({⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}β€˜2) = ((𝐢 βˆ’ 𝐴) / 𝐡))
118106, 117eqtrid 2783 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (π‘Œβ€˜2) = ((𝐢 βˆ’ 𝐴) / 𝐡))
11968fveq1i 6892 . . . . . . . . . . 11 (π‘‹β€˜2) = ({⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}β€˜2)
120 fvpr2g 7191 . . . . . . . . . . . 12 ((2 ∈ V ∧ (𝐢 / 𝐡) ∈ ℝ ∧ 1 β‰  2) β†’ ({⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}β€˜2) = (𝐢 / 𝐡))
121107, 31, 113, 120mp3an2i 1465 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ ({⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}β€˜2) = (𝐢 / 𝐡))
122119, 121eqtrid 2783 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (π‘‹β€˜2) = (𝐢 / 𝐡))
123122adantr 480 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (π‘‹β€˜2) = (𝐢 / 𝐡))
124118, 123oveq12d 7430 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) = (((𝐢 βˆ’ 𝐴) / 𝐡) βˆ’ (𝐢 / 𝐡)))
12529, 1resubcld 11649 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (𝐢 βˆ’ 𝐴) ∈ ℝ)
126125recnd 11249 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (𝐢 βˆ’ 𝐴) ∈ β„‚)
127 divsubdir 11915 . . . . . . . . . . 11 (((𝐢 βˆ’ 𝐴) ∈ β„‚ ∧ 𝐢 ∈ β„‚ ∧ (𝐡 ∈ β„‚ ∧ 𝐡 β‰  0)) β†’ (((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) = (((𝐢 βˆ’ 𝐴) / 𝐡) βˆ’ (𝐢 / 𝐡)))
128126, 45, 49, 127syl3anc 1370 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) = (((𝐢 βˆ’ 𝐴) / 𝐡) βˆ’ (𝐢 / 𝐡)))
129128eqcomd 2737 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (((𝐢 βˆ’ 𝐴) / 𝐡) βˆ’ (𝐢 / 𝐡)) = (((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡))
130129adantr 480 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((𝐢 βˆ’ 𝐴) / 𝐡) βˆ’ (𝐢 / 𝐡)) = (((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡))
131124, 130eqtr2d 2772 . . . . . . 7 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) = ((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)))
132131oveq1d 7427 . . . . . 6 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) = (((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))))
133132oveq1d 7427 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)) = ((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)))
134133eqeq2d 2742 . . . 4 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((π‘β€˜2) = (((((𝐢 βˆ’ 𝐴) βˆ’ 𝐢) / 𝐡) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)) ↔ (π‘β€˜2) = ((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡))))
135105fveq1i 6892 . . . . . . . . . . . . . . 15 (π‘Œβ€˜1) = ({⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}β€˜1)
13670, 70fvpr1 7193 . . . . . . . . . . . . . . . 16 (1 β‰  2 β†’ ({⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}β€˜1) = 1)
13772, 136ax-mp 5 . . . . . . . . . . . . . . 15 ({⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}β€˜1) = 1
138135, 137eqtri 2759 . . . . . . . . . . . . . 14 (π‘Œβ€˜1) = 1
13970, 71fvpr1 7193 . . . . . . . . . . . . . . . 16 (1 β‰  2 β†’ ({⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}β€˜1) = 0)
14072, 139ax-mp 5 . . . . . . . . . . . . . . 15 ({⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}β€˜1) = 0
14169, 140eqtri 2759 . . . . . . . . . . . . . 14 (π‘‹β€˜1) = 0
142138, 141oveq12i 7424 . . . . . . . . . . . . 13 ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1)) = (1 βˆ’ 0)
143 1m0e1 12340 . . . . . . . . . . . . 13 (1 βˆ’ 0) = 1
144142, 143eqtri 2759 . . . . . . . . . . . 12 ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1)) = 1
145144a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1)) = 1)
146145oveq2d 7428 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) = (((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / 1))
147107, 112, 113, 116mp3an2i 1465 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ ({⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}β€˜2) = ((𝐢 βˆ’ 𝐴) / 𝐡))
148106, 147eqtrid 2783 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (π‘Œβ€˜2) = ((𝐢 βˆ’ 𝐴) / 𝐡))
149112recnd 11249 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ ((𝐢 βˆ’ 𝐴) / 𝐡) ∈ β„‚)
150148, 149eqeltrd 2832 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (π‘Œβ€˜2) ∈ β„‚)
151122, 32eqeltrd 2832 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (π‘‹β€˜2) ∈ β„‚)
152150, 151subcld 11578 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ ((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) ∈ β„‚)
153152div1d 11989 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / 1) = ((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)))
154146, 153eqtrd 2771 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) = ((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)))
155154oveq1d 7427 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ ((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) = (((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))))
156155, 122oveq12d 7430 . . . . . . 7 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (π‘‹β€˜2)) = ((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)))
157156adantr 480 . . . . . 6 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (π‘‹β€˜2)) = ((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)))
158157eqcomd 2737 . . . . 5 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)) = (((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (π‘‹β€˜2)))
159158eqeq2d 2742 . . . 4 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ ((π‘β€˜2) = ((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (𝐢 / 𝐡)) ↔ (π‘β€˜2) = (((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (π‘‹β€˜2))))
160104, 134, 1593bitrd 305 . . 3 (((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) β†’ (((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) = 𝐢 ↔ (π‘β€˜2) = (((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (π‘‹β€˜2))))
161160rabbidva 3438 . 2 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ {𝑝 ∈ 𝑃 ∣ ((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) = 𝐢} = {𝑝 ∈ 𝑃 ∣ (π‘β€˜2) = (((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (π‘‹β€˜2))})
162 line2.g . . 3 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) = 𝐢}
163162a1i 11 . 2 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 Β· (π‘β€˜1)) + (𝐡 Β· (π‘β€˜2))) = 𝐢})
16470, 107pm3.2i 470 . . . . . . . 8 (1 ∈ V ∧ 2 ∈ V)
16531, 71jctil 519 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (0 ∈ V ∧ (𝐢 / 𝐡) ∈ ℝ))
166 fprg 7155 . . . . . . . 8 (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ (𝐢 / 𝐡) ∈ ℝ) ∧ 1 β‰  2) β†’ {⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}:{1, 2}⟢{0, (𝐢 / 𝐡)})
167164, 165, 113, 166mp3an2i 1465 . . . . . . 7 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ {⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}:{1, 2}⟢{0, (𝐢 / 𝐡)})
168 0red 11224 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 0 ∈ ℝ)
169168, 31prssd 4825 . . . . . . 7 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ {0, (𝐢 / 𝐡)} βŠ† ℝ)
170167, 169fssd 6735 . . . . . 6 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ {⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}:{1, 2}βŸΆβ„)
17168feq1i 6708 . . . . . 6 (𝑋:{1, 2}βŸΆβ„ ↔ {⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}:{1, 2}βŸΆβ„)
172170, 171sylibr 233 . . . . 5 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝑋:{1, 2}βŸΆβ„)
173 reex 11207 . . . . . 6 ℝ ∈ V
174 prex 5432 . . . . . 6 {1, 2} ∈ V
175173, 174elmap 8871 . . . . 5 (𝑋 ∈ (ℝ ↑m {1, 2}) ↔ 𝑋:{1, 2}βŸΆβ„)
176172, 175sylibr 233 . . . 4 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝑋 ∈ (ℝ ↑m {1, 2}))
1773oveq2i 7423 . . . . 5 (ℝ ↑m 𝐼) = (ℝ ↑m {1, 2})
1784, 177eqtri 2759 . . . 4 𝑃 = (ℝ ↑m {1, 2})
179176, 178eleqtrrdi 2843 . . 3 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝑋 ∈ 𝑃)
180112, 70jctil 519 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (1 ∈ V ∧ ((𝐢 βˆ’ 𝐴) / 𝐡) ∈ ℝ))
181 fprg 7155 . . . . . . . 8 (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ ((𝐢 βˆ’ 𝐴) / 𝐡) ∈ ℝ) ∧ 1 β‰  2) β†’ {⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}:{1, 2}⟢{1, ((𝐢 βˆ’ 𝐴) / 𝐡)})
182164, 180, 113, 181mp3an2i 1465 . . . . . . 7 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ {⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}:{1, 2}⟢{1, ((𝐢 βˆ’ 𝐴) / 𝐡)})
183 1red 11222 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 1 ∈ ℝ)
184183, 112prssd 4825 . . . . . . 7 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ {1, ((𝐢 βˆ’ 𝐴) / 𝐡)} βŠ† ℝ)
185182, 184fssd 6735 . . . . . 6 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ {⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}:{1, 2}βŸΆβ„)
186105feq1i 6708 . . . . . 6 (π‘Œ:{1, 2}βŸΆβ„ ↔ {⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}:{1, 2}βŸΆβ„)
187185, 186sylibr 233 . . . . 5 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ π‘Œ:{1, 2}βŸΆβ„)
188173, 174elmap 8871 . . . . 5 (π‘Œ ∈ (ℝ ↑m {1, 2}) ↔ π‘Œ:{1, 2}βŸΆβ„)
189187, 188sylibr 233 . . . 4 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ π‘Œ ∈ (ℝ ↑m {1, 2}))
190189, 178eleqtrrdi 2843 . . 3 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ π‘Œ ∈ 𝑃)
191 0ne1 12290 . . . . 5 0 β‰  1
19273, 74ax-mp 5 . . . . . . 7 ({⟨1, 0⟩, ⟨2, (𝐢 / 𝐡)⟩}β€˜1) = 0
19369, 192eqtri 2759 . . . . . 6 (π‘‹β€˜1) = 0
19470, 70, 723pm3.2i 1338 . . . . . . . 8 (1 ∈ V ∧ 1 ∈ V ∧ 1 β‰  2)
195 fvpr1g 7190 . . . . . . . 8 ((1 ∈ V ∧ 1 ∈ V ∧ 1 β‰  2) β†’ ({⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}β€˜1) = 1)
196194, 195ax-mp 5 . . . . . . 7 ({⟨1, 1⟩, ⟨2, ((𝐢 βˆ’ 𝐴) / 𝐡)⟩}β€˜1) = 1
197135, 196eqtri 2759 . . . . . 6 (π‘Œβ€˜1) = 1
198193, 197neeq12i 3006 . . . . 5 ((π‘‹β€˜1) β‰  (π‘Œβ€˜1) ↔ 0 β‰  1)
199191, 198mpbir 230 . . . 4 (π‘‹β€˜1) β‰  (π‘Œβ€˜1)
200199a1i 11 . . 3 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (π‘‹β€˜1) β‰  (π‘Œβ€˜1))
201 line2.e . . . 4 𝐸 = (ℝ^β€˜πΌ)
202 line2.l . . . 4 𝐿 = (LineMβ€˜πΈ)
203 eqid 2731 . . . 4 (((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) = (((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1)))
2043, 201, 4, 202, 203rrx2linesl 47591 . . 3 ((𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑃 ∧ (π‘‹β€˜1) β‰  (π‘Œβ€˜1)) β†’ (π‘‹πΏπ‘Œ) = {𝑝 ∈ 𝑃 ∣ (π‘β€˜2) = (((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (π‘‹β€˜2))})
205179, 190, 200, 204syl3anc 1370 . 2 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ (π‘‹πΏπ‘Œ) = {𝑝 ∈ 𝑃 ∣ (π‘β€˜2) = (((((π‘Œβ€˜2) βˆ’ (π‘‹β€˜2)) / ((π‘Œβ€˜1) βˆ’ (π‘‹β€˜1))) Β· ((π‘β€˜1) βˆ’ (π‘‹β€˜1))) + (π‘‹β€˜2))})
206161, 163, 2053eqtr4d 2781 1 ((𝐴 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 𝐡 β‰  0) ∧ 𝐢 ∈ ℝ) β†’ 𝐺 = (π‘‹πΏπ‘Œ))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   β‰  wne 2939  {crab 3431  Vcvv 3473  {cpr 4630  βŸ¨cop 4634  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7412   ↑m cmap 8826  β„‚cc 11114  β„cr 11115  0cc0 11116  1c1 11117   + caddc 11119   Β· cmul 11121   βˆ’ cmin 11451  -cneg 11452   / cdiv 11878  2c2 12274  β„^crrx 25231  LineMcline 47575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194  ax-addf 11195  ax-mulf 11196
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8152  df-tpos 8217  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-er 8709  df-map 8828  df-ixp 8898  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9368  df-sup 9443  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12480  df-z 12566  df-dec 12685  df-uz 12830  df-rp 12982  df-fz 13492  df-seq 13974  df-exp 14035  df-cj 15053  df-re 15054  df-im 15055  df-sqrt 15189  df-abs 15190  df-struct 17087  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-starv 17219  df-sca 17220  df-vsca 17221  df-ip 17222  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-hom 17228  df-cco 17229  df-0g 17394  df-prds 17400  df-pws 17402  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-mhm 18711  df-grp 18864  df-minusg 18865  df-sbg 18866  df-subg 19046  df-ghm 19135  df-cmn 19698  df-abl 19699  df-mgp 20036  df-rng 20054  df-ur 20083  df-ring 20136  df-cring 20137  df-oppr 20232  df-dvdsr 20255  df-unit 20256  df-invr 20286  df-dvr 20299  df-rhm 20370  df-subrng 20442  df-subrg 20467  df-drng 20585  df-field 20586  df-staf 20684  df-srng 20685  df-lmod 20704  df-lss 20775  df-sra 21019  df-rgmod 21020  df-cnfld 21234  df-refld 21468  df-dsmm 21597  df-frlm 21612  df-tng 24413  df-tcph 25017  df-rrx 25233  df-line 47577
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator