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 ⊢ 𝐼 = { 1 , 2 }
line2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
line2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
line2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
line2.g ⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
line2y.x ⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ }
line2y.y ⊢ 𝑌 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑁 ⟩ }
Assertion line2y ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁 ) ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )

Proof

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