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 bicondional is false, RHS is true); 2. C = 0 /\ B =/= 0 : p = (1,-A/B) (LHS of bicondional is true, RHS is false); 3. A = B = C = 0 : p = (1,1) (LHS of bicondional is true, RHS is false). (Contributed by AV, 4-Feb-2023)

Ref Expression
Hypotheses line2ylem.i 
|- I = { 1 , 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 ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) -> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )

Proof

Step Hyp Ref Expression
1 line2ylem.i 
 |-  I = { 1 , 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 ) -> { <. 1 , 0 >. , <. 2 , 0 >. } e. P )
7 5 5 6 mp2an 
 |-  { <. 1 , 0 >. , <. 2 , 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 = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( p ` 1 ) = ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 1 ) )
32 1ex 
 |-  1 e. _V
33 c0ex 
 |-  0 e. _V
34 1ne2 
 |-  1 =/= 2
35 fvpr1g 
 |-  ( ( 1 e. _V /\ 0 e. _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 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( p ` 1 ) = 0 )
38 37 oveq2d 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( A x. ( p ` 1 ) ) = ( A x. 0 ) )
39 fveq1 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( p ` 2 ) = ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 2 ) )
40 2ex 
 |-  2 e. _V
41 fvpr2g 
 |-  ( ( 2 e. _V /\ 0 e. _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 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( p ` 2 ) = 0 )
44 43 oveq2d 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( B x. ( p ` 2 ) ) = ( B x. 0 ) )
45 38 44 oveq12d 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = ( ( A x. 0 ) + ( B x. 0 ) ) )
46 45 eqeq1d 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( ( A x. 0 ) + ( B x. 0 ) ) = C ) )
47 37 eqeq1d 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( ( p ` 1 ) = 0 <-> 0 = 0 ) )
48 46 47 bibi12d 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) <-> ( ( ( A x. 0 ) + ( B x. 0 ) ) = C <-> 0 = 0 ) ) )
49 48 notbid 
 |-  ( p = { <. 1 , 0 >. , <. 2 , 0 >. } -> ( -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) <-> -. ( ( ( A x. 0 ) + ( B x. 0 ) ) = C <-> 0 = 0 ) ) )
50 49 rspcev 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 0 >. } e. P /\ -. ( ( ( A x. 0 ) + ( B x. 0 ) ) = C <-> 0 = 0 ) ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) )
51 7 30 50 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C =/= 0 ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) )
52 51 expcom 
 |-  ( C =/= 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
53 4 52 sylbir 
 |-  ( -. C = 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
54 notnotb 
 |-  ( C = 0 <-> -. -. C = 0 )
55 ianor 
 |-  ( -. ( A =/= 0 /\ B = 0 ) <-> ( -. A =/= 0 \/ -. B = 0 ) )
56 df-ne 
 |-  ( B =/= 0 <-> -. B = 0 )
57 1red 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> 1 e. RR )
58 16 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> A e. RR )
59 58 renegcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> -u A e. RR )
60 19 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> B e. RR )
61 simprl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> B =/= 0 )
62 59 60 61 redivcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> ( -u A / B ) e. RR )
63 1 2 prelrrx2 
 |-  ( ( 1 e. RR /\ ( -u A / B ) e. RR ) -> { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } e. P )
64 57 62 63 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } e. P )
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 mulid1d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. 1 ) = A )
71 70 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> ( A x. 1 ) = A )
72 17 negcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> -u A e. CC )
73 72 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> -u A e. CC )
74 20 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> B e. CC )
75 73 74 61 divcan2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> ( B x. ( -u A / B ) ) = -u A )
76 71 75 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 ) )
77 17 negidd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + -u A ) = 0 )
78 77 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> ( A + -u A ) = 0 )
79 76 78 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> ( ( A x. 1 ) + ( B x. ( -u A / B ) ) ) = 0 )
80 simprr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> C = 0 )
81 79 80 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 ) )
82 81 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 ) ) )
83 69 82 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 ) )
84 fveq1 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( p ` 1 ) = ( { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } ` 1 ) )
85 fvpr1g 
 |-  ( ( 1 e. _V /\ 1 e. _V /\ 1 =/= 2 ) -> ( { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } ` 1 ) = 1 )
86 32 32 34 85 mp3an 
 |-  ( { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } ` 1 ) = 1
87 84 86 eqtrdi 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( p ` 1 ) = 1 )
88 87 oveq2d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( A x. ( p ` 1 ) ) = ( A x. 1 ) )
89 fveq1 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( p ` 2 ) = ( { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } ` 2 ) )
90 ovex 
 |-  ( -u A / B ) e. _V
91 fvpr2g 
 |-  ( ( 2 e. _V /\ ( -u A / B ) e. _V /\ 1 =/= 2 ) -> ( { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } ` 2 ) = ( -u A / B ) )
92 40 90 34 91 mp3an 
 |-  ( { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } ` 2 ) = ( -u A / B )
93 89 92 eqtrdi 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( p ` 2 ) = ( -u A / B ) )
94 93 oveq2d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( B x. ( p ` 2 ) ) = ( B x. ( -u A / B ) ) )
95 88 94 oveq12d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = ( ( A x. 1 ) + ( B x. ( -u A / B ) ) ) )
96 95 eqeq1d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( ( A x. 1 ) + ( B x. ( -u A / B ) ) ) = C ) )
97 87 eqeq1d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( ( p ` 1 ) = 0 <-> 1 = 0 ) )
98 96 97 bibi12d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) <-> ( ( ( A x. 1 ) + ( B x. ( -u A / B ) ) ) = C <-> 1 = 0 ) ) )
99 98 notbid 
 |-  ( p = { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } -> ( -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) <-> -. ( ( ( A x. 1 ) + ( B x. ( -u A / B ) ) ) = C <-> 1 = 0 ) ) )
100 99 rspcev 
 |-  ( ( { <. 1 , 1 >. , <. 2 , ( -u A / B ) >. } e. P /\ -. ( ( ( A x. 1 ) + ( B x. ( -u A / B ) ) ) = C <-> 1 = 0 ) ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) )
101 64 83 100 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( B =/= 0 /\ C = 0 ) ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) )
102 101 expcom 
 |-  ( ( B =/= 0 /\ C = 0 ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
103 102 ex 
 |-  ( B =/= 0 -> ( C = 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) ) )
104 56 103 sylbir 
 |-  ( -. B = 0 -> ( C = 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) ) )
105 notnotb 
 |-  ( B = 0 <-> -. -. B = 0 )
106 nne 
 |-  ( -. A =/= 0 <-> A = 0 )
107 106 bicomi 
 |-  ( A = 0 <-> -. A =/= 0 )
108 1re 
 |-  1 e. RR
109 1 2 prelrrx2 
 |-  ( ( 1 e. RR /\ 1 e. RR ) -> { <. 1 , 1 >. , <. 2 , 1 >. } e. P )
110 108 108 109 mp2an 
 |-  { <. 1 , 1 >. , <. 2 , 1 >. } e. P
111 oveq1 
 |-  ( A = 0 -> ( A x. 1 ) = ( 0 x. 1 ) )
112 111 adantl 
 |-  ( ( B = 0 /\ A = 0 ) -> ( A x. 1 ) = ( 0 x. 1 ) )
113 ax-1cn 
 |-  1 e. CC
114 113 mul02i 
 |-  ( 0 x. 1 ) = 0
115 112 114 eqtrdi 
 |-  ( ( B = 0 /\ A = 0 ) -> ( A x. 1 ) = 0 )
116 oveq1 
 |-  ( B = 0 -> ( B x. 1 ) = ( 0 x. 1 ) )
117 116 adantr 
 |-  ( ( B = 0 /\ A = 0 ) -> ( B x. 1 ) = ( 0 x. 1 ) )
118 117 114 eqtrdi 
 |-  ( ( B = 0 /\ A = 0 ) -> ( B x. 1 ) = 0 )
119 115 118 oveq12d 
 |-  ( ( B = 0 /\ A = 0 ) -> ( ( A x. 1 ) + ( B x. 1 ) ) = ( 0 + 0 ) )
120 119 23 eqtrdi 
 |-  ( ( B = 0 /\ A = 0 ) -> ( ( A x. 1 ) + ( B x. 1 ) ) = 0 )
121 id 
 |-  ( C = 0 -> C = 0 )
122 120 121 eqeqan12d 
 |-  ( ( ( B = 0 /\ A = 0 ) /\ C = 0 ) -> ( ( ( A x. 1 ) + ( B x. 1 ) ) = C <-> 0 = 0 ) )
123 122 bibi1d 
 |-  ( ( ( B = 0 /\ A = 0 ) /\ C = 0 ) -> ( ( ( ( A x. 1 ) + ( B x. 1 ) ) = C <-> 1 = 0 ) <-> ( 0 = 0 <-> 1 = 0 ) ) )
124 69 123 mtbiri 
 |-  ( ( ( B = 0 /\ A = 0 ) /\ C = 0 ) -> -. ( ( ( A x. 1 ) + ( B x. 1 ) ) = C <-> 1 = 0 ) )
125 fveq1 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( p ` 1 ) = ( { <. 1 , 1 >. , <. 2 , 1 >. } ` 1 ) )
126 fvpr1g 
 |-  ( ( 1 e. _V /\ 1 e. _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 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( p ` 1 ) = 1 )
129 128 oveq2d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( A x. ( p ` 1 ) ) = ( A x. 1 ) )
130 fveq1 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( p ` 2 ) = ( { <. 1 , 1 >. , <. 2 , 1 >. } ` 2 ) )
131 fvpr2g 
 |-  ( ( 2 e. _V /\ 1 e. _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 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( p ` 2 ) = 1 )
134 133 oveq2d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( B x. ( p ` 2 ) ) = ( B x. 1 ) )
135 129 134 oveq12d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = ( ( A x. 1 ) + ( B x. 1 ) ) )
136 135 eqeq1d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( ( A x. 1 ) + ( B x. 1 ) ) = C ) )
137 128 eqeq1d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( ( p ` 1 ) = 0 <-> 1 = 0 ) )
138 136 137 bibi12d 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) <-> ( ( ( A x. 1 ) + ( B x. 1 ) ) = C <-> 1 = 0 ) ) )
139 138 notbid 
 |-  ( p = { <. 1 , 1 >. , <. 2 , 1 >. } -> ( -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) <-> -. ( ( ( A x. 1 ) + ( B x. 1 ) ) = C <-> 1 = 0 ) ) )
140 139 rspcev 
 |-  ( ( { <. 1 , 1 >. , <. 2 , 1 >. } e. P /\ -. ( ( ( A x. 1 ) + ( B x. 1 ) ) = C <-> 1 = 0 ) ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) )
141 110 124 140 sylancr 
 |-  ( ( ( B = 0 /\ A = 0 ) /\ C = 0 ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) )
142 141 a1d 
 |-  ( ( ( B = 0 /\ A = 0 ) /\ C = 0 ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
143 142 ex 
 |-  ( ( B = 0 /\ A = 0 ) -> ( C = 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) ) )
144 105 107 143 syl2anbr 
 |-  ( ( -. -. B = 0 /\ -. A =/= 0 ) -> ( C = 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) ) )
145 104 144 jaoi3 
 |-  ( ( -. B = 0 \/ -. A =/= 0 ) -> ( C = 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) ) )
146 145 orcoms 
 |-  ( ( -. A =/= 0 \/ -. B = 0 ) -> ( C = 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) ) )
147 55 146 sylbi 
 |-  ( -. ( A =/= 0 /\ B = 0 ) -> ( C = 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) ) )
148 147 com12 
 |-  ( C = 0 -> ( -. ( A =/= 0 /\ B = 0 ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) ) )
149 54 148 sylbir 
 |-  ( -. -. C = 0 -> ( -. ( A =/= 0 /\ B = 0 ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) ) )
150 149 imp 
 |-  ( ( -. -. C = 0 /\ -. ( A =/= 0 /\ B = 0 ) ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
151 53 150 jaoi3 
 |-  ( ( -. C = 0 \/ -. ( A =/= 0 /\ B = 0 ) ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
152 151 orcoms 
 |-  ( ( -. ( A =/= 0 /\ B = 0 ) \/ -. C = 0 ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
153 152 com12 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( -. ( A =/= 0 /\ B = 0 ) \/ -. C = 0 ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
154 3 153 syl5bi 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. ( ( A =/= 0 /\ B = 0 ) /\ C = 0 ) -> E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
155 rexnal 
 |-  ( E. p e. P -. ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) <-> -. A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) )
156 154 155 syl6ib 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. ( ( A =/= 0 /\ B = 0 ) /\ C = 0 ) -> -. A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
157 156 con4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) -> ( ( A =/= 0 /\ B = 0 ) /\ C = 0 ) ) )
158 df-3an 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) <-> ( ( A =/= 0 /\ B = 0 ) /\ C = 0 ) )
159 157 158 syl6ibr 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) -> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )