Metamath Proof Explorer

Theorem line2ylem

Description: Lemma for line2y . This proof is based on counterexamples for the following cases: 1. C =/= 0 : p = (0,0) (LHS of biconditional is false, RHS is true); 2. C = 0 /\ B =/= 0 : p = (1,-A/B) (LHS of biconditional is true, RHS is false); 3. A = B = C = 0 : p = (1,1) (LHS of biconditional is true, RHS is false). (Contributed by AV, 4-Feb-2023)

Ref Expression
Hypotheses line2ylem.i ⊢ 𝐼 = { 1 , 2 }
line2ylem.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
Assertion line2ylem ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 line2ylem.i ⊢ 𝐼 = { 1 , 2 }
2 line2ylem.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3 ianor ⊢ ( ¬ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) ↔ ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∨ ¬ 𝐶 = 0 ) )
4 df-ne ⊢ ( 𝐶 ≠ 0 ↔ ¬ 𝐶 = 0 )
5 0re ⊢ 0 ∈ ℝ
6 1 2 prelrrx2 ⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∈ 𝑃 )
7 5 5 6 mp2an ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∈ 𝑃
8 eqneqall ⊢ ( 𝐶 = 0 → ( 𝐶 ≠ 0 → ¬ 0 = 0 ) )
9 8 com12 ⊢ ( 𝐶 ≠ 0 → ( 𝐶 = 0 → ¬ 0 = 0 ) )
10 eqid ⊢ 0 = 0
11 10 pm2.24i ⊢ ( ¬ 0 = 0 → 𝐶 = 0 )
12 9 11 impbid1 ⊢ ( 𝐶 ≠ 0 → ( 𝐶 = 0 ↔ ¬ 0 = 0 ) )
13 12 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ( 𝐶 = 0 ↔ ¬ 0 = 0 ) )
14 xor3 ⊢ ( ¬ ( 𝐶 = 0 ↔ 0 = 0 ) ↔ ( 𝐶 = 0 ↔ ¬ 0 = 0 ) )
15 13 14 sylibr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ¬ ( 𝐶 = 0 ↔ 0 = 0 ) )
16 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
17 16 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
18 17 mul01d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 0 ) = 0 )
19 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
20 19 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
21 20 mul01d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 0 ) = 0 )
22 18 21 oveq12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = ( 0 + 0 ) )
23 00id ⊢ ( 0 + 0 ) = 0
24 22 23 eqtrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 0 )
25 24 eqeq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 𝐶 ) )
26 eqcom ⊢ ( 0 = 𝐶 ↔ 𝐶 = 0 )
27 25 26 bitrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 𝐶 = 0 ) )
28 27 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 𝐶 = 0 ) )
29 28 bibi1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ( ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ↔ ( 𝐶 = 0 ↔ 0 = 0 ) ) )
30 15 29 mtbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ¬ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) )
31 fveq1 ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝑝 ‘ 1 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) )
32 1ex ⊢ 1 ∈ V
33 c0ex ⊢ 0 ∈ V
34 1ne2 ⊢ 1 ≠ 2
35 fvpr1g ⊢ ( ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) = 0 )
36 32 33 34 35 mp3an ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) = 0
37 31 36 eqtrdi ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝑝 ‘ 1 ) = 0 )
38 37 oveq2d ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · 0 ) )
39 fveq1 ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝑝 ‘ 2 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) )
40 2ex ⊢ 2 ∈ V
41 fvpr2g ⊢ ( ( 2 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) = 0 )
42 40 33 34 41 mp3an ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) = 0
43 39 42 eqtrdi ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝑝 ‘ 2 ) = 0 )
44 43 oveq2d ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 𝐵 · 0 ) )
45 38 44 oveq12d ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) )
46 45 eqeq1d ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ) )
47 37 eqeq1d ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ( 𝑝 ‘ 1 ) = 0 ↔ 0 = 0 ) )
48 46 47 bibi12d ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ) )
49 48 notbid ⊢ ( 𝑝 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ¬ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ) )
50 49 rspcev ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∈ 𝑃 ∧ ¬ ( ( ( 𝐴 · 0 ) + ( 𝐵 · 0 ) ) = 𝐶 ↔ 0 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
51 7 30 50 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≠ 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
52 51 expcom ⊢ ( 𝐶 ≠ 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
53 4 52 sylbir ⊢ ( ¬ 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
54 notnotb ⊢ ( 𝐶 = 0 ↔ ¬ ¬ 𝐶 = 0 )
55 ianor ⊢ ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ↔ ( ¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0 ) )
56 df-ne ⊢ ( 𝐵 ≠ 0 ↔ ¬ 𝐵 = 0 )
57 1red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 1 ∈ ℝ )
58 16 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐴 ∈ ℝ )
59 58 renegcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → - 𝐴 ∈ ℝ )
60 19 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐵 ∈ ℝ )
61 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐵 ≠ 0 )
62 59 60 61 redivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( - 𝐴 / 𝐵 ) ∈ ℝ )
63 1 2 prelrrx2 ⊢ ( ( 1 ∈ ℝ ∧ ( - 𝐴 / 𝐵 ) ∈ ℝ ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ∈ 𝑃 )
64 57 62 63 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ∈ 𝑃 )
65 ax-1ne0 ⊢ 1 ≠ 0
66 65 neii ⊢ ¬ 1 = 0
67 10 66 2th ⊢ ( 0 = 0 ↔ ¬ 1 = 0 )
68 xor3 ⊢ ( ¬ ( 0 = 0 ↔ 1 = 0 ) ↔ ( 0 = 0 ↔ ¬ 1 = 0 ) )
69 67 68 mpbir ⊢ ¬ ( 0 = 0 ↔ 1 = 0 )
70 17 mulridd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 1 ) = 𝐴 )
71 70 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( 𝐴 · 1 ) = 𝐴 )
72 17 negcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → - 𝐴 ∈ ℂ )
73 72 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → - 𝐴 ∈ ℂ )
74 20 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐵 ∈ ℂ )
75 73 74 61 divcan2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( 𝐵 · ( - 𝐴 / 𝐵 ) ) = - 𝐴 )
76 71 75 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = ( 𝐴 + - 𝐴 ) )
77 17 negidd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + - 𝐴 ) = 0 )
78 77 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( 𝐴 + - 𝐴 ) = 0 )
79 76 78 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 0 )
80 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → 𝐶 = 0 )
81 79 80 eqeq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 0 = 0 ) )
82 81 bibi1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ( ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ↔ ( 0 = 0 ↔ 1 = 0 ) ) )
83 69 82 mtbiri ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) )
84 fveq1 ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝑝 ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 1 ) )
85 fvpr1g ⊢ ( ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 1 ) = 1 )
86 32 32 34 85 mp3an ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 1 ) = 1
87 84 86 eqtrdi ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝑝 ‘ 1 ) = 1 )
88 87 oveq2d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · 1 ) )
89 fveq1 ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝑝 ‘ 2 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 2 ) )
90 ovex ⊢ ( - 𝐴 / 𝐵 ) ∈ V
91 fvpr2g ⊢ ( ( 2 ∈ V ∧ ( - 𝐴 / 𝐵 ) ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 2 ) = ( - 𝐴 / 𝐵 ) )
92 40 90 34 91 mp3an ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ‘ 2 ) = ( - 𝐴 / 𝐵 )
93 89 92 eqtrdi ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝑝 ‘ 2 ) = ( - 𝐴 / 𝐵 ) )
94 93 oveq2d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 𝐵 · ( - 𝐴 / 𝐵 ) ) )
95 88 94 oveq12d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) )
96 95 eqeq1d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ) )
97 87 eqeq1d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ( 𝑝 ‘ 1 ) = 0 ↔ 1 = 0 ) )
98 96 97 bibi12d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ) )
99 98 notbid ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ) )
100 99 rspcev ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( - 𝐴 / 𝐵 ) ⟩ } ∈ 𝑃 ∧ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · ( - 𝐴 / 𝐵 ) ) ) = 𝐶 ↔ 1 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
101 64 83 100 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
102 101 expcom ⊢ ( ( 𝐵 ≠ 0 ∧ 𝐶 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
103 102 ex ⊢ ( 𝐵 ≠ 0 → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
104 56 103 sylbir ⊢ ( ¬ 𝐵 = 0 → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
105 notnotb ⊢ ( 𝐵 = 0 ↔ ¬ ¬ 𝐵 = 0 )
106 nne ⊢ ( ¬ 𝐴 ≠ 0 ↔ 𝐴 = 0 )
107 106 bicomi ⊢ ( 𝐴 = 0 ↔ ¬ 𝐴 ≠ 0 )
108 1re ⊢ 1 ∈ ℝ
109 1 2 prelrrx2 ⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 )
110 108 108 109 mp2an ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃
111 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · 1 ) = ( 0 · 1 ) )
112 111 adantl ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐴 · 1 ) = ( 0 · 1 ) )
113 ax-1cn ⊢ 1 ∈ ℂ
114 113 mul02i ⊢ ( 0 · 1 ) = 0
115 112 114 eqtrdi ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐴 · 1 ) = 0 )
116 oveq1 ⊢ ( 𝐵 = 0 → ( 𝐵 · 1 ) = ( 0 · 1 ) )
117 116 adantr ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐵 · 1 ) = ( 0 · 1 ) )
118 117 114 eqtrdi ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐵 · 1 ) = 0 )
119 115 118 oveq12d ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = ( 0 + 0 ) )
120 119 23 eqtrdi ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 0 )
121 id ⊢ ( 𝐶 = 0 → 𝐶 = 0 )
122 120 121 eqeqan12d ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 0 = 0 ) )
123 122 bibi1d ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ( ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ↔ ( 0 = 0 ↔ 1 = 0 ) ) )
124 69 123 mtbiri ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) )
125 fveq1 ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑝 ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) )
126 fvpr1g ⊢ ( ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 1 )
127 32 32 34 126 mp3an ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 1
128 125 127 eqtrdi ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑝 ‘ 1 ) = 1 )
129 128 oveq2d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · 1 ) )
130 fveq1 ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑝 ‘ 2 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) )
131 fvpr2g ⊢ ( ( 2 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1 )
132 40 32 34 131 mp3an ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1
133 130 132 eqtrdi ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑝 ‘ 2 ) = 1 )
134 133 oveq2d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 𝐵 · 1 ) )
135 129 134 oveq12d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) )
136 135 eqeq1d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ) )
137 128 eqeq1d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( 𝑝 ‘ 1 ) = 0 ↔ 1 = 0 ) )
138 136 137 bibi12d ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ) )
139 138 notbid ⊢ ( 𝑝 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ) )
140 139 rspcev ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 ∧ ¬ ( ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) = 𝐶 ↔ 1 = 0 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
141 110 124 140 sylancr ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
142 141 a1d ⊢ ( ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) ∧ 𝐶 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
143 142 ex ⊢ ( ( 𝐵 = 0 ∧ 𝐴 = 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
144 105 107 143 syl2anbr ⊢ ( ( ¬ ¬ 𝐵 = 0 ∧ ¬ 𝐴 ≠ 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
145 104 144 jaoi3 ⊢ ( ( ¬ 𝐵 = 0 ∨ ¬ 𝐴 ≠ 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
146 145 orcoms ⊢ ( ( ¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
147 55 146 sylbi ⊢ ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) → ( 𝐶 = 0 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
148 147 com12 ⊢ ( 𝐶 = 0 → ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
149 54 148 sylbir ⊢ ( ¬ ¬ 𝐶 = 0 → ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) ) )
150 149 imp ⊢ ( ( ¬ ¬ 𝐶 = 0 ∧ ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
151 53 150 jaoi3 ⊢ ( ( ¬ 𝐶 = 0 ∨ ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
152 151 orcoms ⊢ ( ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∨ ¬ 𝐶 = 0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
153 152 com12 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ¬ ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∨ ¬ 𝐶 = 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
154 3 153 biimtrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
155 rexnal ⊢ ( ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ↔ ¬ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) )
156 154 155 imbitrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) → ¬ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) ) )
157 156 con4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) → ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) ) )
158 df-3an ⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ↔ ( ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ) ∧ 𝐶 = 0 ) )
159 157 158 imbitrrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 0 ) → ( 𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0 ) ) )