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 
|- I = ( 0 ..^ 2 )
line2ylem.p 
|- P = ( RR ^m I )
Assertion line2ylem 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 0 ) = 0 ) -> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )

Proof

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