Metamath Proof Explorer

Theorem line2y

Description: Example for a vertical line G passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023)

Ref Expression
Hypotheses line2.i ⊢ 𝐼 = ( 0 ..^ 2 )
line2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
line2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
line2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
line2.g ⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 }
line2y.x ⊢ 𝑋 = ⟨“ 0 𝑀 ”⟩
line2y.y ⊢ 𝑌 = ⟨“ 0 𝑁 ”⟩
Assertion line2y ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 line2.i ⊢ 𝐼 = ( 0 ..^ 2 )
2 line2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 line2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 line2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
5 line2.g ⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 }
6 line2y.x ⊢ 𝑋 = ⟨“ 0 𝑀 ”⟩
7 line2y.y ⊢ 𝑌 = ⟨“ 0 𝑁 ”⟩
8 5 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } )
9 s2len ⊢ ( ♯ ‘ ⟨“ 0 𝑀 ”⟩ ) = 2
10 9 eqcomi ⊢ 2 = ( ♯ ‘ ⟨“ 0 𝑀 ”⟩ )
11 10 a1i ⊢ ( 𝑀 ∈ ℝ → 2 = ( ♯ ‘ ⟨“ 0 𝑀 ”⟩ ) )
12 0red ⊢ ( 𝑀 ∈ ℝ → 0 ∈ ℝ )
13 id ⊢ ( 𝑀 ∈ ℝ → 𝑀 ∈ ℝ )
14 12 13 s2cld ⊢ ( 𝑀 ∈ ℝ → ⟨“ 0 𝑀 ”⟩ ∈ Word ℝ )
15 11 14 wrdfd ⊢ ( 𝑀 ∈ ℝ → ⟨“ 0 𝑀 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ )
16 1 feq2i ⊢ ( ⟨“ 0 𝑀 ”⟩ : 𝐼 ⟶ ℝ ↔ ⟨“ 0 𝑀 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ )
17 15 16 sylibr ⊢ ( 𝑀 ∈ ℝ → ⟨“ 0 𝑀 ”⟩ : 𝐼 ⟶ ℝ )
18 reex ⊢ ℝ ∈ V
19 1 ovexi ⊢ 𝐼 ∈ V
20 18 19 elmap ⊢ ( ⟨“ 0 𝑀 ”⟩ ∈ ( ℝ ↑m 𝐼 ) ↔ ⟨“ 0 𝑀 ”⟩ : 𝐼 ⟶ ℝ )
21 17 20 sylibr ⊢ ( 𝑀 ∈ ℝ → ⟨“ 0 𝑀 ”⟩ ∈ ( ℝ ↑m 𝐼 ) )
22 21 6 3 3eltr4g ⊢ ( 𝑀 ∈ ℝ → 𝑋 ∈ 𝑃 )
23 22 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → 𝑋 ∈ 𝑃 )
24 s2len ⊢ ( ♯ ‘ ⟨“ 0 𝑁 ”⟩ ) = 2
25 24 eqcomi ⊢ 2 = ( ♯ ‘ ⟨“ 0 𝑁 ”⟩ )
26 25 a1i ⊢ ( 𝑁 ∈ ℝ → 2 = ( ♯ ‘ ⟨“ 0 𝑁 ”⟩ ) )
27 0red ⊢ ( 𝑁 ∈ ℝ → 0 ∈ ℝ )
28 id ⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
29 27 28 s2cld ⊢ ( 𝑁 ∈ ℝ → ⟨“ 0 𝑁 ”⟩ ∈ Word ℝ )
30 26 29 wrdfd ⊢ ( 𝑁 ∈ ℝ → ⟨“ 0 𝑁 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ )
31 1 feq2i ⊢ ( ⟨“ 0 𝑁 ”⟩ : 𝐼 ⟶ ℝ ↔ ⟨“ 0 𝑁 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ )
32 30 31 sylibr ⊢ ( 𝑁 ∈ ℝ → ⟨“ 0 𝑁 ”⟩ : 𝐼 ⟶ ℝ )
33 18 19 pm3.2i ⊢ ( ℝ ∈ V ∧ 𝐼 ∈ V )
34 elmapg ⊢ ( ( ℝ ∈ V ∧ 𝐼 ∈ V ) → ( ⟨“ 0 𝑁 ”⟩ ∈ ( ℝ ↑m 𝐼 ) ↔ ⟨“ 0 𝑁 ”⟩ : 𝐼 ⟶ ℝ ) )
35 33 34 mp1i ⊢ ( 𝑁 ∈ ℝ → ( ⟨“ 0 𝑁 ”⟩ ∈ ( ℝ ↑m 𝐼 ) ↔ ⟨“ 0 𝑁 ”⟩ : 𝐼 ⟶ ℝ ) )
36 32 35 mpbird ⊢ ( 𝑁 ∈ ℝ → ⟨“ 0 𝑁 ”⟩ ∈ ( ℝ ↑m 𝐼 ) )
37 36 7 3 3eltr4g ⊢ ( 𝑁 ∈ ℝ → 𝑌 ∈ 𝑃 )
38 37 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → 𝑌 ∈ 𝑃 )
39 6 fveq1i ⊢ ( 𝑋 ‘ 0 ) = ( ⟨“ 0 𝑀 ”⟩ ‘ 0 )
40 0re ⊢ 0 ∈ ℝ
41 s2fv0 ⊢ ( 0 ∈ ℝ → ( ⟨“ 0 𝑀 ”⟩ ‘ 0 ) = 0 )
42 40 41 mp1i ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( ⟨“ 0 𝑀 ”⟩ ‘ 0 ) = 0 )
43 39 42 eqtrid ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ‘ 0 ) = 0 )
44 7 fveq1i ⊢ ( 𝑌 ‘ 0 ) = ( ⟨“ 0 𝑁 ”⟩ ‘ 0 )
45 s2fv0 ⊢ ( 0 ∈ ℝ → ( ⟨“ 0 𝑁 ”⟩ ‘ 0 ) = 0 )
46 40 45 mp1i ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( ⟨“ 0 𝑁 ”⟩ ‘ 0 ) = 0 )
47 44 46 eqtrid ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑌 ‘ 0 ) = 0 )
48 43 47 eqtr4d ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) )
49 simp3 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → 𝑀 ≠ 𝑁 )
50 6 fveq1i ⊢ ( 𝑋 ‘ 1 ) = ( ⟨“ 0 𝑀 ”⟩ ‘ 1 )
51 s2fv1 ⊢ ( 𝑀 ∈ ℝ → ( ⟨“ 0 𝑀 ”⟩ ‘ 1 ) = 𝑀 )
52 51 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( ⟨“ 0 𝑀 ”⟩ ‘ 1 ) = 𝑀 )
53 50 52 eqtrid ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ‘ 1 ) = 𝑀 )
54 7 fveq1i ⊢ ( 𝑌 ‘ 1 ) = ( ⟨“ 0 𝑁 ”⟩ ‘ 1 )
55 s2fv1 ⊢ ( 𝑁 ∈ ℝ → ( ⟨“ 0 𝑁 ”⟩ ‘ 1 ) = 𝑁 )
56 55 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( ⟨“ 0 𝑁 ”⟩ ‘ 1 ) = 𝑁 )
57 54 56 eqtrid ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑌 ‘ 1 ) = 𝑁 )
58 49 53 57 3netr4d ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
59 48 58 jca ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) )
60 23 38 59 3jca ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) )
61 60 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) )
62 1 2 3 4 rrx2vlinest ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) } )
63 61 62 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) } )
64 8 63 eqeq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) } ) )
65 40 41 ax-mp ⊢ ( ⟨“ 0 𝑀 ”⟩ ‘ 0 ) = 0
66 39 65 eqtri ⊢ ( 𝑋 ‘ 0 ) = 0
67 66 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝑋 ‘ 0 ) = 0 )
68 67 eqeq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ↔ ( 𝑝 ‘ 0 ) = 0 ) )
69 68 rabbidv ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = 0 } )
70 69 eqeq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) } ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = 0 } ) )
71 rabbi ⊢ ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = 0 } )
72 1 3 line2ylem ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )
73 72 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )
74 oveq1 ⊢ ( 𝐵 = 0 → ( 𝐵 · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
75 74 3ad2ant2 ⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ( 𝐵 · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
76 75 oveq2d ⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 0 · ( 𝑝 ‘ 1 ) ) ) )
77 simp3 ⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → 𝐶 = 0 )
78 76 77 eqeq12d ⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 0 · ( 𝑝 ‘ 1 ) ) ) = 0 ) )
79 78 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 0 · ( 𝑝 ‘ 1 ) ) ) = 0 ) )
80 1 3 rrx2pyel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
81 80 recnd ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
82 81 mul02d ⊢ ( 𝑝 ∈ 𝑃 → ( 0 · ( 𝑝 ‘ 1 ) ) = 0 )
83 82 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 · ( 𝑝 ‘ 1 ) ) = 0 )
84 83 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 0 · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + 0 ) )
85 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
86 85 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
87 86 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐴 ∈ ℂ )
88 1 3 rrx2pxel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℝ )
89 88 recnd ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℂ )
90 89 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 0 ) ∈ ℂ )
91 87 90 mulcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 0 ) ) ∈ ℂ )
92 91 addridd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + 0 ) = ( 𝐴 · ( 𝑝 ‘ 0 ) ) )
93 84 92 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 0 · ( 𝑝 ‘ 1 ) ) ) = ( 𝐴 · ( 𝑝 ‘ 0 ) ) )
94 93 eqeq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 0 · ( 𝑝 ‘ 1 ) ) ) = 0 ↔ ( 𝐴 · ( 𝑝 ‘ 0 ) ) = 0 ) )
95 87 90 mul0ord ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) = 0 ↔ ( 𝐴 = 0 ∨ ( 𝑝 ‘ 0 ) = 0 ) ) )
96 eqneqall ⊢ ( 𝐴 = 0 → ( 𝐴 ≠ 0 → ( 𝑝 ‘ 0 ) = 0 ) )
97 96 com12 ⊢ ( 𝐴 ≠ 0 → ( 𝐴 = 0 → ( 𝑝 ‘ 0 ) = 0 ) )
98 97 3ad2ant1 ⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ( 𝐴 = 0 → ( 𝑝 ‘ 0 ) = 0 ) )
99 98 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 = 0 → ( 𝑝 ‘ 0 ) = 0 ) )
100 idd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 0 ) = 0 → ( 𝑝 ‘ 0 ) = 0 ) )
101 99 100 jaod ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 = 0 ∨ ( 𝑝 ‘ 0 ) = 0 ) → ( 𝑝 ‘ 0 ) = 0 ) )
102 olc ⊢ ( ( 𝑝 ‘ 0 ) = 0 → ( 𝐴 = 0 ∨ ( 𝑝 ‘ 0 ) = 0 ) )
103 101 102 impbid1 ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 = 0 ∨ ( 𝑝 ‘ 0 ) = 0 ) ↔ ( 𝑝 ‘ 0 ) = 0 ) )
104 95 103 bitrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) = 0 ↔ ( 𝑝 ‘ 0 ) = 0 ) )
105 79 94 104 3bitrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) )
106 105 ralrimiva ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) )
107 106 ex ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ) )
108 73 107 impbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 0 ) = 0 ) ↔ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )
109 71 108 bitr3id ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = 0 } ↔ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )
110 64 70 109 3bitrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )