Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  line2xlem Structured version   Visualization version   GIF version

Theorem line2xlem 47714
Description: Lemma for line2x 47715. This proof is based on counterexamples for the following cases: 1. ๐‘€ โ‰  (๐ถ / ๐ต): p = (0,C/B) (LHS of bicondional is true, RHS is false); 2. ๐ด โ‰  0 โˆง ๐‘€ = (๐ถ / ๐ต): p = (1,C/B) (LHS of bicondional is false, RHS is true). (Contributed by AV, 4-Feb-2023.)
Hypotheses
Ref Expression
line2.i ๐ผ = {1, 2}
line2.e ๐ธ = (โ„^โ€˜๐ผ)
line2.p ๐‘ƒ = (โ„ โ†‘m ๐ผ)
line2.l ๐ฟ = (LineMโ€˜๐ธ)
line2.g ๐บ = {๐‘ โˆˆ ๐‘ƒ โˆฃ ((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ}
line2x.x ๐‘‹ = {โŸจ1, 0โŸฉ, โŸจ2, ๐‘€โŸฉ}
line2x.y ๐‘Œ = {โŸจ1, 1โŸฉ, โŸจ2, ๐‘€โŸฉ}
Assertion
Ref Expression
line2xlem (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€) โ†’ (๐ด = 0 โˆง ๐‘€ = (๐ถ / ๐ต))))
Distinct variable groups:   ๐ด,๐‘   ๐ต,๐‘   ๐ถ,๐‘   ๐ธ,๐‘   ๐ผ,๐‘   ๐‘ƒ,๐‘   ๐‘‹,๐‘   ๐‘Œ,๐‘   ๐‘€,๐‘
Allowed substitution hints:   ๐บ(๐‘)   ๐ฟ(๐‘)

Proof of Theorem line2xlem
StepHypRef Expression
1 ianor 978 . . . 4 (ยฌ (๐ด = 0 โˆง ๐‘€ = (๐ถ / ๐ต)) โ†” (ยฌ ๐ด = 0 โˆจ ยฌ ๐‘€ = (๐ถ / ๐ต)))
2 df-ne 2935 . . . . 5 (๐ด โ‰  0 โ†” ยฌ ๐ด = 0)
3 df-ne 2935 . . . . 5 (๐‘€ โ‰  (๐ถ / ๐ต) โ†” ยฌ ๐‘€ = (๐ถ / ๐ต))
42, 3orbi12i 911 . . . 4 ((๐ด โ‰  0 โˆจ ๐‘€ โ‰  (๐ถ / ๐ต)) โ†” (ยฌ ๐ด = 0 โˆจ ยฌ ๐‘€ = (๐ถ / ๐ต)))
51, 4bitr4i 278 . . 3 (ยฌ (๐ด = 0 โˆง ๐‘€ = (๐ถ / ๐ต)) โ†” (๐ด โ‰  0 โˆจ ๐‘€ โ‰  (๐ถ / ๐ต)))
6 0red 11221 . . . . . . . . . 10 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ 0 โˆˆ โ„)
7 simp3 1135 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ ๐ถ โˆˆ โ„)
87adantr 480 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ๐ถ โˆˆ โ„)
9 simpl 482 . . . . . . . . . . . . . 14 ((๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โ†’ ๐ต โˆˆ โ„)
1093ad2ant2 1131 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ ๐ต โˆˆ โ„)
1110adantr 480 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ๐ต โˆˆ โ„)
12 simp2r 1197 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ ๐ต โ‰  0)
1312adantr 480 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ๐ต โ‰  0)
148, 11, 13redivcld 12046 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ถ / ๐ต) โˆˆ โ„)
1514adantl 481 . . . . . . . . . 10 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ (๐ถ / ๐ต) โˆˆ โ„)
16 line2.i . . . . . . . . . . 11 ๐ผ = {1, 2}
17 line2.p . . . . . . . . . . 11 ๐‘ƒ = (โ„ โ†‘m ๐ผ)
1816, 17prelrrx2 47674 . . . . . . . . . 10 ((0 โˆˆ โ„ โˆง (๐ถ / ๐ต) โˆˆ โ„) โ†’ {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โˆˆ ๐‘ƒ)
196, 15, 18syl2anc 583 . . . . . . . . 9 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โˆˆ ๐‘ƒ)
20 id 22 . . . . . . . . . . . . . . . 16 (๐‘€ โ‰  (๐ถ / ๐ต) โ†’ ๐‘€ โ‰  (๐ถ / ๐ต))
2120necomd 2990 . . . . . . . . . . . . . . 15 (๐‘€ โ‰  (๐ถ / ๐ต) โ†’ (๐ถ / ๐ต) โ‰  ๐‘€)
2221neneqd 2939 . . . . . . . . . . . . . 14 (๐‘€ โ‰  (๐ถ / ๐ต) โ†’ ยฌ (๐ถ / ๐ต) = ๐‘€)
2322a1d 25 . . . . . . . . . . . . 13 (๐‘€ โ‰  (๐ถ / ๐ต) โ†’ (๐ถ = ๐ถ โ†’ ยฌ (๐ถ / ๐ต) = ๐‘€))
24 eqidd 2727 . . . . . . . . . . . . . 14 (ยฌ (๐ถ / ๐ต) = ๐‘€ โ†’ ๐ถ = ๐ถ)
2524a1i 11 . . . . . . . . . . . . 13 (๐‘€ โ‰  (๐ถ / ๐ต) โ†’ (ยฌ (๐ถ / ๐ต) = ๐‘€ โ†’ ๐ถ = ๐ถ))
2623, 25impbid 211 . . . . . . . . . . . 12 (๐‘€ โ‰  (๐ถ / ๐ต) โ†’ (๐ถ = ๐ถ โ†” ยฌ (๐ถ / ๐ต) = ๐‘€))
27 xor3 382 . . . . . . . . . . . 12 (ยฌ (๐ถ = ๐ถ โ†” (๐ถ / ๐ต) = ๐‘€) โ†” (๐ถ = ๐ถ โ†” ยฌ (๐ถ / ๐ต) = ๐‘€))
2826, 27sylibr 233 . . . . . . . . . . 11 (๐‘€ โ‰  (๐ถ / ๐ต) โ†’ ยฌ (๐ถ = ๐ถ โ†” (๐ถ / ๐ต) = ๐‘€))
2928adantr 480 . . . . . . . . . 10 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ยฌ (๐ถ = ๐ถ โ†” (๐ถ / ๐ต) = ๐‘€))
30 0red 11221 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ 0 โˆˆ โ„)
31 fv1prop 47660 . . . . . . . . . . . . . . . . . 18 (0 โˆˆ โ„ โ†’ ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1) = 0)
3230, 31syl 17 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1) = 0)
3332oveq2d 7421 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) = (๐ด ยท 0))
34 recn 11202 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚)
3534mul01d 11417 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„ โ†’ (๐ด ยท 0) = 0)
36353ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท 0) = 0)
3736adantr 480 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ด ยท 0) = 0)
3833, 37eqtrd 2766 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) = 0)
39 ovexd 7440 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ถ / ๐ต) โˆˆ V)
40 fv2prop 47661 . . . . . . . . . . . . . . . . . 18 ((๐ถ / ๐ต) โˆˆ V โ†’ ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = (๐ถ / ๐ต))
4139, 40syl 17 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = (๐ถ / ๐ต))
4241oveq2d 7421 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2)) = (๐ต ยท (๐ถ / ๐ต)))
437recnd 11246 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ ๐ถ โˆˆ โ„‚)
4443adantr 480 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ๐ถ โˆˆ โ„‚)
459recnd 11246 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โ†’ ๐ต โˆˆ โ„‚)
46453ad2ant2 1131 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ ๐ต โˆˆ โ„‚)
4746adantr 480 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ๐ต โˆˆ โ„‚)
4844, 47, 13divcan2d 11996 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ต ยท (๐ถ / ๐ต)) = ๐ถ)
4942, 48eqtrd 2766 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2)) = ๐ถ)
5038, 49oveq12d 7423 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = (0 + ๐ถ))
5150adantl 481 . . . . . . . . . . . . 13 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = (0 + ๐ถ))
5243addlidd 11419 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ (0 + ๐ถ) = ๐ถ)
5352adantr 480 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (0 + ๐ถ) = ๐ถ)
5453adantl 481 . . . . . . . . . . . . 13 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ (0 + ๐ถ) = ๐ถ)
5551, 54eqtrd 2766 . . . . . . . . . . . 12 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ)
5655eqeq1d 2728 . . . . . . . . . . 11 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ (((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ๐ถ = ๐ถ))
5741eqeq1d 2728 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€ โ†” (๐ถ / ๐ต) = ๐‘€))
5857adantl 481 . . . . . . . . . . 11 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ (({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€ โ†” (๐ถ / ๐ต) = ๐‘€))
5956, 58bibi12d 345 . . . . . . . . . 10 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ((((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€) โ†” (๐ถ = ๐ถ โ†” (๐ถ / ๐ต) = ๐‘€)))
6029, 59mtbird 325 . . . . . . . . 9 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ยฌ (((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€))
61 fveq1 6884 . . . . . . . . . . . . . . 15 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (๐‘โ€˜1) = ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1))
6261oveq2d 7421 . . . . . . . . . . . . . 14 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (๐ด ยท (๐‘โ€˜1)) = (๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)))
63 fveq1 6884 . . . . . . . . . . . . . . 15 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (๐‘โ€˜2) = ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))
6463oveq2d 7421 . . . . . . . . . . . . . 14 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (๐ต ยท (๐‘โ€˜2)) = (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2)))
6562, 64oveq12d 7423 . . . . . . . . . . . . 13 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ ((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))))
6665eqeq1d 2728 . . . . . . . . . . . 12 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” ((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ))
6763eqeq1d 2728 . . . . . . . . . . . 12 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ ((๐‘โ€˜2) = ๐‘€ โ†” ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€))
6866, 67bibi12d 345 . . . . . . . . . . 11 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ ((((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€) โ†” (((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€)))
6968notbid 318 . . . . . . . . . 10 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€) โ†” ยฌ (((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€)))
7069rspcev 3606 . . . . . . . . 9 (({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โˆˆ ๐‘ƒ โˆง ยฌ (((๐ด ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 0โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€))
7119, 60, 70syl2anc 583 . . . . . . . 8 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€))
7271ex 412 . . . . . . 7 (๐‘€ โ‰  (๐ถ / ๐ต) โ†’ (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€)))
73 nne 2938 . . . . . . . 8 (ยฌ ๐‘€ โ‰  (๐ถ / ๐ต) โ†” ๐‘€ = (๐ถ / ๐ต))
74 1red 11219 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ 1 โˆˆ โ„)
757, 10, 12redivcld 12046 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ถ / ๐ต) โˆˆ โ„)
7674, 75jca 511 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ (1 โˆˆ โ„ โˆง (๐ถ / ๐ต) โˆˆ โ„))
7776adantr 480 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (1 โˆˆ โ„ โˆง (๐ถ / ๐ต) โˆˆ โ„))
7816, 17prelrrx2 47674 . . . . . . . . . . . 12 ((1 โˆˆ โ„ โˆง (๐ถ / ๐ต) โˆˆ โ„) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โˆˆ ๐‘ƒ)
7977, 78syl 17 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โˆˆ ๐‘ƒ)
8079adantl 481 . . . . . . . . . 10 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โˆˆ ๐‘ƒ)
81 eqneqall 2945 . . . . . . . . . . . . . . . . 17 (๐ด = 0 โ†’ (๐ด โ‰  0 โ†’ ยฌ (๐ถ / ๐ต) = ๐‘€))
8281com12 32 . . . . . . . . . . . . . . . 16 (๐ด โ‰  0 โ†’ (๐ด = 0 โ†’ ยฌ (๐ถ / ๐ต) = ๐‘€))
8382adantl 481 . . . . . . . . . . . . . . 15 ((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โ†’ (๐ด = 0 โ†’ ยฌ (๐ถ / ๐ต) = ๐‘€))
84 pm2.24 124 . . . . . . . . . . . . . . . . 17 ((๐ถ / ๐ต) = ๐‘€ โ†’ (ยฌ (๐ถ / ๐ต) = ๐‘€ โ†’ ๐ด = 0))
8584eqcoms 2734 . . . . . . . . . . . . . . . 16 (๐‘€ = (๐ถ / ๐ต) โ†’ (ยฌ (๐ถ / ๐ต) = ๐‘€ โ†’ ๐ด = 0))
8685adantr 480 . . . . . . . . . . . . . . 15 ((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โ†’ (ยฌ (๐ถ / ๐ต) = ๐‘€ โ†’ ๐ด = 0))
8783, 86impbid 211 . . . . . . . . . . . . . 14 ((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โ†’ (๐ด = 0 โ†” ยฌ (๐ถ / ๐ต) = ๐‘€))
88 xor3 382 . . . . . . . . . . . . . 14 (ยฌ (๐ด = 0 โ†” (๐ถ / ๐ต) = ๐‘€) โ†” (๐ด = 0 โ†” ยฌ (๐ถ / ๐ต) = ๐‘€))
8987, 88sylibr 233 . . . . . . . . . . . . 13 ((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โ†’ ยฌ (๐ด = 0 โ†” (๐ถ / ๐ต) = ๐‘€))
9089adantr 480 . . . . . . . . . . . 12 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ยฌ (๐ด = 0 โ†” (๐ถ / ๐ต) = ๐‘€))
91 simprl1 1215 . . . . . . . . . . . . . . . . 17 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ๐ด โˆˆ โ„)
9291recnd 11246 . . . . . . . . . . . . . . . 16 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ๐ด โˆˆ โ„‚)
938adantl 481 . . . . . . . . . . . . . . . . 17 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ๐ถ โˆˆ โ„)
9493recnd 11246 . . . . . . . . . . . . . . . 16 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ๐ถ โˆˆ โ„‚)
9592, 94addcomd 11420 . . . . . . . . . . . . . . 15 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ (๐ด + ๐ถ) = (๐ถ + ๐ด))
9695eqeq1d 2728 . . . . . . . . . . . . . 14 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ((๐ด + ๐ถ) = ๐ถ โ†” (๐ถ + ๐ด) = ๐ถ))
97 recn 11202 . . . . . . . . . . . . . . . . . . 19 (๐ถ โˆˆ โ„ โ†’ ๐ถ โˆˆ โ„‚)
9834, 97anim12ci 613 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚))
99983adant2 1128 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚))
10099adantr 480 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚))
101100adantl 481 . . . . . . . . . . . . . . 15 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ (๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚))
102 addid0 11637 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ถ + ๐ด) = ๐ถ โ†” ๐ด = 0))
103101, 102syl 17 . . . . . . . . . . . . . 14 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ((๐ถ + ๐ด) = ๐ถ โ†” ๐ด = 0))
10496, 103bitrd 279 . . . . . . . . . . . . 13 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ((๐ด + ๐ถ) = ๐ถ โ†” ๐ด = 0))
105104bibi1d 343 . . . . . . . . . . . 12 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ (((๐ด + ๐ถ) = ๐ถ โ†” (๐ถ / ๐ต) = ๐‘€) โ†” (๐ด = 0 โ†” (๐ถ / ๐ต) = ๐‘€)))
10690, 105mtbird 325 . . . . . . . . . . 11 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ยฌ ((๐ด + ๐ถ) = ๐ถ โ†” (๐ถ / ๐ต) = ๐‘€))
107 1ex 11214 . . . . . . . . . . . . . . . . . . . 20 1 โˆˆ V
108107a1i 11 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ 1 โˆˆ V)
109 fv1prop 47660 . . . . . . . . . . . . . . . . . . 19 (1 โˆˆ V โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1) = 1)
110108, 109syl 17 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1) = 1)
111110oveq2d 7421 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) = (๐ด ยท 1))
112 ax-1rid 11182 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„ โ†’ (๐ด ยท 1) = ๐ด)
1131123ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท 1) = ๐ด)
114113adantr 480 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ด ยท 1) = ๐ด)
115111, 114eqtrd 2766 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) = ๐ด)
116 fv2prop 47661 . . . . . . . . . . . . . . . . . . 19 ((๐ถ / ๐ต) โˆˆ V โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = (๐ถ / ๐ต))
11739, 116syl 17 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = (๐ถ / ๐ต))
118117oveq2d 7421 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2)) = (๐ต ยท (๐ถ / ๐ต)))
1198recnd 11246 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ๐ถ โˆˆ โ„‚)
120119, 47, 13divcan2d 11996 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ต ยท (๐ถ / ๐ต)) = ๐ถ)
121118, 120eqtrd 2766 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2)) = ๐ถ)
122115, 121oveq12d 7423 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = (๐ด + ๐ถ))
123122eqeq1d 2728 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” (๐ด + ๐ถ) = ๐ถ))
124117eqeq1d 2728 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€ โ†” (๐ถ / ๐ต) = ๐‘€))
125123, 124bibi12d 345 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ((((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€) โ†” ((๐ด + ๐ถ) = ๐ถ โ†” (๐ถ / ๐ต) = ๐‘€)))
126125notbid 318 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (ยฌ (((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€) โ†” ยฌ ((๐ด + ๐ถ) = ๐ถ โ†” (๐ถ / ๐ต) = ๐‘€)))
127126adantl 481 . . . . . . . . . . 11 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ (ยฌ (((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€) โ†” ยฌ ((๐ด + ๐ถ) = ๐ถ โ†” (๐ถ / ๐ต) = ๐‘€)))
128106, 127mpbird 257 . . . . . . . . . 10 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ ยฌ (((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€))
129 fveq1 6884 . . . . . . . . . . . . . . . 16 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (๐‘โ€˜1) = ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1))
130129oveq2d 7421 . . . . . . . . . . . . . . 15 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (๐ด ยท (๐‘โ€˜1)) = (๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)))
131 fveq1 6884 . . . . . . . . . . . . . . . 16 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (๐‘โ€˜2) = ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))
132131oveq2d 7421 . . . . . . . . . . . . . . 15 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (๐ต ยท (๐‘โ€˜2)) = (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2)))
133130, 132oveq12d 7423 . . . . . . . . . . . . . 14 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ ((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))))
134133eqeq1d 2728 . . . . . . . . . . . . 13 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” ((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ))
135131eqeq1d 2728 . . . . . . . . . . . . 13 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ ((๐‘โ€˜2) = ๐‘€ โ†” ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€))
136134, 135bibi12d 345 . . . . . . . . . . . 12 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ ((((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€) โ†” (((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€)))
137136notbid 318 . . . . . . . . . . 11 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โ†’ (ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€) โ†” ยฌ (((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€)))
138137rspcev 3606 . . . . . . . . . 10 (({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ} โˆˆ ๐‘ƒ โˆง ยฌ (((๐ด ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜1)) + (๐ต ยท ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2))) = ๐ถ โ†” ({โŸจ1, 1โŸฉ, โŸจ2, (๐ถ / ๐ต)โŸฉ}โ€˜2) = ๐‘€)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€))
13980, 128, 138syl2anc 583 . . . . . . . . 9 (((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โˆง ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€))
140139ex 412 . . . . . . . 8 ((๐‘€ = (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โ†’ (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€)))
14173, 140sylanb 580 . . . . . . 7 ((ยฌ ๐‘€ โ‰  (๐ถ / ๐ต) โˆง ๐ด โ‰  0) โ†’ (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€)))
14272, 141jaoi3 1057 . . . . . 6 ((๐‘€ โ‰  (๐ถ / ๐ต) โˆจ ๐ด โ‰  0) โ†’ (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€)))
143142orcoms 869 . . . . 5 ((๐ด โ‰  0 โˆจ ๐‘€ โ‰  (๐ถ / ๐ต)) โ†’ (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€)))
144143com12 32 . . . 4 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ((๐ด โ‰  0 โˆจ ๐‘€ โ‰  (๐ถ / ๐ต)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€)))
145 rexnal 3094 . . . 4 (โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€) โ†” ยฌ โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€))
146144, 145imbitrdi 250 . . 3 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ ((๐ด โ‰  0 โˆจ ๐‘€ โ‰  (๐ถ / ๐ต)) โ†’ ยฌ โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€)))
1475, 146biimtrid 241 . 2 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (ยฌ (๐ด = 0 โˆง ๐‘€ = (๐ถ / ๐ต)) โ†’ ยฌ โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€)))
148147con4d 115 1 (((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โˆง ๐ถ โˆˆ โ„) โˆง ๐‘€ โˆˆ โ„) โ†’ (โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜2) = ๐‘€) โ†’ (๐ด = 0 โˆง ๐‘€ = (๐ถ / ๐ต))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2934  โˆ€wral 3055  โˆƒwrex 3064  {crab 3426  Vcvv 3468  {cpr 4625  โŸจcop 4629  โ€˜cfv 6537  (class class class)co 7405   โ†‘m cmap 8822  โ„‚cc 11110  โ„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   ยท cmul 11117   / cdiv 11875  2c2 12271  โ„^crrx 25266  LineMcline 47688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-po 5581  df-so 5582  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-2 12279
This theorem is referenced by:  line2x  47715
  Copyright terms: Public domain W3C validator