Metamath Proof Explorer


Theorem line2xlem

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

Ref Expression
Hypotheses line2.i I = 1 2
line2.e E = I
line2.p P = I
line2.l L = Line M E
line2.g G = p P | A p 1 + B p 2 = C
line2x.x X = 1 0 2 M
line2x.y Y = 1 1 2 M
Assertion line2xlem A B B 0 C M p P A p 1 + B p 2 = C p 2 = M A = 0 M = C B

Proof

Step Hyp Ref Expression
1 line2.i I = 1 2
2 line2.e E = I
3 line2.p P = I
4 line2.l L = Line M E
5 line2.g G = p P | A p 1 + B p 2 = C
6 line2x.x X = 1 0 2 M
7 line2x.y Y = 1 1 2 M
8 ianor ¬ A = 0 M = C B ¬ A = 0 ¬ M = C B
9 df-ne A 0 ¬ A = 0
10 df-ne M C B ¬ M = C B
11 9 10 orbi12i A 0 M C B ¬ A = 0 ¬ M = C B
12 8 11 bitr4i ¬ A = 0 M = C B A 0 M C B
13 0red M C B A B B 0 C M 0
14 simp3 A B B 0 C C
15 14 adantr A B B 0 C M C
16 simpl B B 0 B
17 16 3ad2ant2 A B B 0 C B
18 17 adantr A B B 0 C M B
19 simp2r A B B 0 C B 0
20 19 adantr A B B 0 C M B 0
21 15 18 20 redivcld A B B 0 C M C B
22 21 adantl M C B A B B 0 C M C B
23 1 3 prelrrx2 0 C B 1 0 2 C B P
24 13 22 23 syl2anc M C B A B B 0 C M 1 0 2 C B P
25 id M C B M C B
26 25 necomd M C B C B M
27 26 neneqd M C B ¬ C B = M
28 27 a1d M C B C = C ¬ C B = M
29 eqidd ¬ C B = M C = C
30 29 a1i M C B ¬ C B = M C = C
31 28 30 impbid M C B C = C ¬ C B = M
32 xor3 ¬ C = C C B = M C = C ¬ C B = M
33 31 32 sylibr M C B ¬ C = C C B = M
34 33 adantr M C B A B B 0 C M ¬ C = C C B = M
35 0red A B B 0 C M 0
36 fv1prop 0 1 0 2 C B 1 = 0
37 35 36 syl A B B 0 C M 1 0 2 C B 1 = 0
38 37 oveq2d A B B 0 C M A 1 0 2 C B 1 = A 0
39 recn A A
40 39 mul01d A A 0 = 0
41 40 3ad2ant1 A B B 0 C A 0 = 0
42 41 adantr A B B 0 C M A 0 = 0
43 38 42 eqtrd A B B 0 C M A 1 0 2 C B 1 = 0
44 ovexd A B B 0 C M C B V
45 fv2prop C B V 1 0 2 C B 2 = C B
46 44 45 syl A B B 0 C M 1 0 2 C B 2 = C B
47 46 oveq2d A B B 0 C M B 1 0 2 C B 2 = B C B
48 14 recnd A B B 0 C C
49 48 adantr A B B 0 C M C
50 16 recnd B B 0 B
51 50 3ad2ant2 A B B 0 C B
52 51 adantr A B B 0 C M B
53 49 52 20 divcan2d A B B 0 C M B C B = C
54 47 53 eqtrd A B B 0 C M B 1 0 2 C B 2 = C
55 43 54 oveq12d A B B 0 C M A 1 0 2 C B 1 + B 1 0 2 C B 2 = 0 + C
56 55 adantl M C B A B B 0 C M A 1 0 2 C B 1 + B 1 0 2 C B 2 = 0 + C
57 48 addid2d A B B 0 C 0 + C = C
58 57 adantr A B B 0 C M 0 + C = C
59 58 adantl M C B A B B 0 C M 0 + C = C
60 56 59 eqtrd M C B A B B 0 C M A 1 0 2 C B 1 + B 1 0 2 C B 2 = C
61 60 eqeq1d M C B A B B 0 C M A 1 0 2 C B 1 + B 1 0 2 C B 2 = C C = C
62 46 eqeq1d A B B 0 C M 1 0 2 C B 2 = M C B = M
63 62 adantl M C B A B B 0 C M 1 0 2 C B 2 = M C B = M
64 61 63 bibi12d M C B A B B 0 C M A 1 0 2 C B 1 + B 1 0 2 C B 2 = C 1 0 2 C B 2 = M C = C C B = M
65 34 64 mtbird M C B A B B 0 C M ¬ A 1 0 2 C B 1 + B 1 0 2 C B 2 = C 1 0 2 C B 2 = M
66 fveq1 p = 1 0 2 C B p 1 = 1 0 2 C B 1
67 66 oveq2d p = 1 0 2 C B A p 1 = A 1 0 2 C B 1
68 fveq1 p = 1 0 2 C B p 2 = 1 0 2 C B 2
69 68 oveq2d p = 1 0 2 C B B p 2 = B 1 0 2 C B 2
70 67 69 oveq12d p = 1 0 2 C B A p 1 + B p 2 = A 1 0 2 C B 1 + B 1 0 2 C B 2
71 70 eqeq1d p = 1 0 2 C B A p 1 + B p 2 = C A 1 0 2 C B 1 + B 1 0 2 C B 2 = C
72 68 eqeq1d p = 1 0 2 C B p 2 = M 1 0 2 C B 2 = M
73 71 72 bibi12d p = 1 0 2 C B A p 1 + B p 2 = C p 2 = M A 1 0 2 C B 1 + B 1 0 2 C B 2 = C 1 0 2 C B 2 = M
74 73 notbid p = 1 0 2 C B ¬ A p 1 + B p 2 = C p 2 = M ¬ A 1 0 2 C B 1 + B 1 0 2 C B 2 = C 1 0 2 C B 2 = M
75 74 rspcev 1 0 2 C B P ¬ A 1 0 2 C B 1 + B 1 0 2 C B 2 = C 1 0 2 C B 2 = M p P ¬ A p 1 + B p 2 = C p 2 = M
76 24 65 75 syl2anc M C B A B B 0 C M p P ¬ A p 1 + B p 2 = C p 2 = M
77 76 ex M C B A B B 0 C M p P ¬ A p 1 + B p 2 = C p 2 = M
78 nne ¬ M C B M = C B
79 1red A B B 0 C 1
80 14 17 19 redivcld A B B 0 C C B
81 79 80 jca A B B 0 C 1 C B
82 81 adantr A B B 0 C M 1 C B
83 1 3 prelrrx2 1 C B 1 1 2 C B P
84 82 83 syl A B B 0 C M 1 1 2 C B P
85 84 adantl M = C B A 0 A B B 0 C M 1 1 2 C B P
86 eqneqall A = 0 A 0 ¬ C B = M
87 86 com12 A 0 A = 0 ¬ C B = M
88 87 adantl M = C B A 0 A = 0 ¬ C B = M
89 pm2.24 C B = M ¬ C B = M A = 0
90 89 eqcoms M = C B ¬ C B = M A = 0
91 90 adantr M = C B A 0 ¬ C B = M A = 0
92 88 91 impbid M = C B A 0 A = 0 ¬ C B = M
93 xor3 ¬ A = 0 C B = M A = 0 ¬ C B = M
94 92 93 sylibr M = C B A 0 ¬ A = 0 C B = M
95 94 adantr M = C B A 0 A B B 0 C M ¬ A = 0 C B = M
96 simprl1 M = C B A 0 A B B 0 C M A
97 96 recnd M = C B A 0 A B B 0 C M A
98 15 adantl M = C B A 0 A B B 0 C M C
99 98 recnd M = C B A 0 A B B 0 C M C
100 97 99 addcomd M = C B A 0 A B B 0 C M A + C = C + A
101 100 eqeq1d M = C B A 0 A B B 0 C M A + C = C C + A = C
102 recn C C
103 39 102 anim12ci A C C A
104 103 3adant2 A B B 0 C C A
105 104 adantr A B B 0 C M C A
106 105 adantl M = C B A 0 A B B 0 C M C A
107 addid0 C A C + A = C A = 0
108 106 107 syl M = C B A 0 A B B 0 C M C + A = C A = 0
109 101 108 bitrd M = C B A 0 A B B 0 C M A + C = C A = 0
110 109 bibi1d M = C B A 0 A B B 0 C M A + C = C C B = M A = 0 C B = M
111 95 110 mtbird M = C B A 0 A B B 0 C M ¬ A + C = C C B = M
112 1ex 1 V
113 112 a1i A B B 0 C M 1 V
114 fv1prop 1 V 1 1 2 C B 1 = 1
115 113 114 syl A B B 0 C M 1 1 2 C B 1 = 1
116 115 oveq2d A B B 0 C M A 1 1 2 C B 1 = A 1
117 ax-1rid A A 1 = A
118 117 3ad2ant1 A B B 0 C A 1 = A
119 118 adantr A B B 0 C M A 1 = A
120 116 119 eqtrd A B B 0 C M A 1 1 2 C B 1 = A
121 fv2prop C B V 1 1 2 C B 2 = C B
122 44 121 syl A B B 0 C M 1 1 2 C B 2 = C B
123 122 oveq2d A B B 0 C M B 1 1 2 C B 2 = B C B
124 15 recnd A B B 0 C M C
125 124 52 20 divcan2d A B B 0 C M B C B = C
126 123 125 eqtrd A B B 0 C M B 1 1 2 C B 2 = C
127 120 126 oveq12d A B B 0 C M A 1 1 2 C B 1 + B 1 1 2 C B 2 = A + C
128 127 eqeq1d A B B 0 C M A 1 1 2 C B 1 + B 1 1 2 C B 2 = C A + C = C
129 122 eqeq1d A B B 0 C M 1 1 2 C B 2 = M C B = M
130 128 129 bibi12d A B B 0 C M A 1 1 2 C B 1 + B 1 1 2 C B 2 = C 1 1 2 C B 2 = M A + C = C C B = M
131 130 notbid A B B 0 C M ¬ A 1 1 2 C B 1 + B 1 1 2 C B 2 = C 1 1 2 C B 2 = M ¬ A + C = C C B = M
132 131 adantl M = C B A 0 A B B 0 C M ¬ A 1 1 2 C B 1 + B 1 1 2 C B 2 = C 1 1 2 C B 2 = M ¬ A + C = C C B = M
133 111 132 mpbird M = C B A 0 A B B 0 C M ¬ A 1 1 2 C B 1 + B 1 1 2 C B 2 = C 1 1 2 C B 2 = M
134 fveq1 p = 1 1 2 C B p 1 = 1 1 2 C B 1
135 134 oveq2d p = 1 1 2 C B A p 1 = A 1 1 2 C B 1
136 fveq1 p = 1 1 2 C B p 2 = 1 1 2 C B 2
137 136 oveq2d p = 1 1 2 C B B p 2 = B 1 1 2 C B 2
138 135 137 oveq12d p = 1 1 2 C B A p 1 + B p 2 = A 1 1 2 C B 1 + B 1 1 2 C B 2
139 138 eqeq1d p = 1 1 2 C B A p 1 + B p 2 = C A 1 1 2 C B 1 + B 1 1 2 C B 2 = C
140 136 eqeq1d p = 1 1 2 C B p 2 = M 1 1 2 C B 2 = M
141 139 140 bibi12d p = 1 1 2 C B A p 1 + B p 2 = C p 2 = M A 1 1 2 C B 1 + B 1 1 2 C B 2 = C 1 1 2 C B 2 = M
142 141 notbid p = 1 1 2 C B ¬ A p 1 + B p 2 = C p 2 = M ¬ A 1 1 2 C B 1 + B 1 1 2 C B 2 = C 1 1 2 C B 2 = M
143 142 rspcev 1 1 2 C B P ¬ A 1 1 2 C B 1 + B 1 1 2 C B 2 = C 1 1 2 C B 2 = M p P ¬ A p 1 + B p 2 = C p 2 = M
144 85 133 143 syl2anc M = C B A 0 A B B 0 C M p P ¬ A p 1 + B p 2 = C p 2 = M
145 144 ex M = C B A 0 A B B 0 C M p P ¬ A p 1 + B p 2 = C p 2 = M
146 78 145 sylanb ¬ M C B A 0 A B B 0 C M p P ¬ A p 1 + B p 2 = C p 2 = M
147 77 146 jaoi3 M C B A 0 A B B 0 C M p P ¬ A p 1 + B p 2 = C p 2 = M
148 147 orcoms A 0 M C B A B B 0 C M p P ¬ A p 1 + B p 2 = C p 2 = M
149 148 com12 A B B 0 C M A 0 M C B p P ¬ A p 1 + B p 2 = C p 2 = M
150 rexnal p P ¬ A p 1 + B p 2 = C p 2 = M ¬ p P A p 1 + B p 2 = C p 2 = M
151 149 150 syl6ib A B B 0 C M A 0 M C B ¬ p P A p 1 + B p 2 = C p 2 = M
152 12 151 syl5bi A B B 0 C M ¬ A = 0 M = C B ¬ p P A p 1 + B p 2 = C p 2 = M
153 152 con4d A B B 0 C M p P A p 1 + B p 2 = C p 2 = M A = 0 M = C B