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

Theorem line2ylem 47427
Description: Lemma for line2y 47431. This proof is based on counterexamples for the following cases: 1. ๐ถ โ‰  0: p = (0,0) (LHS of bicondional is false, RHS is true); 2. ๐ถ = 0 โˆง ๐ต โ‰  0: p = (1,-A/B) (LHS of bicondional is true, RHS is false); 3. ๐ด = ๐ต = ๐ถ = 0: p = (1,1) (LHS of bicondional is true, RHS is false). (Contributed by AV, 4-Feb-2023.)
Hypotheses
Ref Expression
line2ylem.i ๐ผ = {1, 2}
line2ylem.p ๐‘ƒ = (โ„ โ†‘m ๐ผ)
Assertion
Ref Expression
line2ylem ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†’ (๐ด โ‰  0 โˆง ๐ต = 0 โˆง ๐ถ = 0)))
Distinct variable groups:   ๐ด,๐‘   ๐ต,๐‘   ๐ถ,๐‘   ๐‘ƒ,๐‘
Allowed substitution hint:   ๐ผ(๐‘)

Proof of Theorem line2ylem
StepHypRef Expression
1 ianor 980 . . . . 5 (ยฌ ((๐ด โ‰  0 โˆง ๐ต = 0) โˆง ๐ถ = 0) โ†” (ยฌ (๐ด โ‰  0 โˆง ๐ต = 0) โˆจ ยฌ ๐ถ = 0))
2 df-ne 2941 . . . . . . . . 9 (๐ถ โ‰  0 โ†” ยฌ ๐ถ = 0)
3 0re 11215 . . . . . . . . . . . 12 0 โˆˆ โ„
4 line2ylem.i . . . . . . . . . . . . 13 ๐ผ = {1, 2}
5 line2ylem.p . . . . . . . . . . . . 13 ๐‘ƒ = (โ„ โ†‘m ๐ผ)
64, 5prelrrx2 47389 . . . . . . . . . . . 12 ((0 โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โˆˆ ๐‘ƒ)
73, 3, 6mp2an 690 . . . . . . . . . . 11 {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โˆˆ ๐‘ƒ
8 eqneqall 2951 . . . . . . . . . . . . . . . 16 (๐ถ = 0 โ†’ (๐ถ โ‰  0 โ†’ ยฌ 0 = 0))
98com12 32 . . . . . . . . . . . . . . 15 (๐ถ โ‰  0 โ†’ (๐ถ = 0 โ†’ ยฌ 0 = 0))
10 eqid 2732 . . . . . . . . . . . . . . . 16 0 = 0
1110pm2.24i 150 . . . . . . . . . . . . . . 15 (ยฌ 0 = 0 โ†’ ๐ถ = 0)
129, 11impbid1 224 . . . . . . . . . . . . . 14 (๐ถ โ‰  0 โ†’ (๐ถ = 0 โ†” ยฌ 0 = 0))
1312adantl 482 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ (๐ถ = 0 โ†” ยฌ 0 = 0))
14 xor3 383 . . . . . . . . . . . . 13 (ยฌ (๐ถ = 0 โ†” 0 = 0) โ†” (๐ถ = 0 โ†” ยฌ 0 = 0))
1513, 14sylibr 233 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ ยฌ (๐ถ = 0 โ†” 0 = 0))
16 simp1 1136 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ๐ด โˆˆ โ„)
1716recnd 11241 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ๐ด โˆˆ โ„‚)
1817mul01d 11412 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท 0) = 0)
19 simp2 1137 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ๐ต โˆˆ โ„)
2019recnd 11241 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ๐ต โˆˆ โ„‚)
2120mul01d 11412 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต ยท 0) = 0)
2218, 21oveq12d 7426 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยท 0) + (๐ต ยท 0)) = (0 + 0))
23 00id 11388 . . . . . . . . . . . . . . . . 17 (0 + 0) = 0
2422, 23eqtrdi 2788 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยท 0) + (๐ต ยท 0)) = 0)
2524eqeq1d 2734 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = ๐ถ))
26 eqcom 2739 . . . . . . . . . . . . . . 15 (0 = ๐ถ โ†” ๐ถ = 0)
2725, 26bitrdi 286 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” ๐ถ = 0))
2827adantr 481 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” ๐ถ = 0))
2928bibi1d 343 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ ((((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = 0) โ†” (๐ถ = 0 โ†” 0 = 0)))
3015, 29mtbird 324 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ ยฌ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = 0))
31 fveq1 6890 . . . . . . . . . . . . . . . . . 18 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐‘โ€˜1) = ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜1))
32 1ex 11209 . . . . . . . . . . . . . . . . . . 19 1 โˆˆ V
33 c0ex 11207 . . . . . . . . . . . . . . . . . . 19 0 โˆˆ V
34 1ne2 12419 . . . . . . . . . . . . . . . . . . 19 1 โ‰  2
35 fvpr1g 7187 . . . . . . . . . . . . . . . . . . 19 ((1 โˆˆ V โˆง 0 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜1) = 0)
3632, 33, 34, 35mp3an 1461 . . . . . . . . . . . . . . . . . 18 ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜1) = 0
3731, 36eqtrdi 2788 . . . . . . . . . . . . . . . . 17 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐‘โ€˜1) = 0)
3837oveq2d 7424 . . . . . . . . . . . . . . . 16 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐ด ยท (๐‘โ€˜1)) = (๐ด ยท 0))
39 fveq1 6890 . . . . . . . . . . . . . . . . . 18 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐‘โ€˜2) = ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜2))
40 2ex 12288 . . . . . . . . . . . . . . . . . . 19 2 โˆˆ V
41 fvpr2g 7188 . . . . . . . . . . . . . . . . . . 19 ((2 โˆˆ V โˆง 0 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜2) = 0)
4240, 33, 34, 41mp3an 1461 . . . . . . . . . . . . . . . . . 18 ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜2) = 0
4339, 42eqtrdi 2788 . . . . . . . . . . . . . . . . 17 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐‘โ€˜2) = 0)
4443oveq2d 7424 . . . . . . . . . . . . . . . 16 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐ต ยท (๐‘โ€˜2)) = (๐ต ยท 0))
4538, 44oveq12d 7426 . . . . . . . . . . . . . . 15 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ ((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ((๐ด ยท 0) + (๐ต ยท 0)))
4645eqeq1d 2734 . . . . . . . . . . . . . 14 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” ((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ))
4737eqeq1d 2734 . . . . . . . . . . . . . 14 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ ((๐‘โ€˜1) = 0 โ†” 0 = 0))
4846, 47bibi12d 345 . . . . . . . . . . . . 13 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ ((((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†” (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = 0)))
4948notbid 317 . . . . . . . . . . . 12 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†” ยฌ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = 0)))
5049rspcev 3612 . . . . . . . . . . 11 (({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โˆˆ ๐‘ƒ โˆง ยฌ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = 0)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
517, 30, 50sylancr 587 . . . . . . . . . 10 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
5251expcom 414 . . . . . . . . 9 (๐ถ โ‰  0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
532, 52sylbir 234 . . . . . . . 8 (ยฌ ๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
54 notnotb 314 . . . . . . . . . 10 (๐ถ = 0 โ†” ยฌ ยฌ ๐ถ = 0)
55 ianor 980 . . . . . . . . . . . 12 (ยฌ (๐ด โ‰  0 โˆง ๐ต = 0) โ†” (ยฌ ๐ด โ‰  0 โˆจ ยฌ ๐ต = 0))
56 df-ne 2941 . . . . . . . . . . . . . . 15 (๐ต โ‰  0 โ†” ยฌ ๐ต = 0)
57 1red 11214 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ 1 โˆˆ โ„)
5816adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ด โˆˆ โ„)
5958renegcld 11640 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ -๐ด โˆˆ โ„)
6019adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ต โˆˆ โ„)
61 simprl 769 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ต โ‰  0)
6259, 60, 61redivcld 12041 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (-๐ด / ๐ต) โˆˆ โ„)
634, 5prelrrx2 47389 . . . . . . . . . . . . . . . . . . 19 ((1 โˆˆ โ„ โˆง (-๐ด / ๐ต) โˆˆ โ„) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โˆˆ ๐‘ƒ)
6457, 62, 63syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โˆˆ ๐‘ƒ)
65 ax-1ne0 11178 . . . . . . . . . . . . . . . . . . . . . 22 1 โ‰  0
6665neii 2942 . . . . . . . . . . . . . . . . . . . . 21 ยฌ 1 = 0
6710, 662th 263 . . . . . . . . . . . . . . . . . . . 20 (0 = 0 โ†” ยฌ 1 = 0)
68 xor3 383 . . . . . . . . . . . . . . . . . . . 20 (ยฌ (0 = 0 โ†” 1 = 0) โ†” (0 = 0 โ†” ยฌ 1 = 0))
6967, 68mpbir 230 . . . . . . . . . . . . . . . . . . 19 ยฌ (0 = 0 โ†” 1 = 0)
7017mulridd 11230 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท 1) = ๐ด)
7170adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (๐ด ยท 1) = ๐ด)
7217negcld 11557 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ -๐ด โˆˆ โ„‚)
7372adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ -๐ด โˆˆ โ„‚)
7420adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ต โˆˆ โ„‚)
7573, 74, 61divcan2d 11991 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (๐ต ยท (-๐ด / ๐ต)) = -๐ด)
7671, 75oveq12d 7426 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = (๐ด + -๐ด))
7717negidd 11560 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด + -๐ด) = 0)
7877adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (๐ด + -๐ด) = 0)
7976, 78eqtrd 2772 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = 0)
80 simprr 771 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ถ = 0)
8179, 80eqeq12d 2748 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 0 = 0))
8281bibi1d 343 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ((((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 1 = 0) โ†” (0 = 0 โ†” 1 = 0)))
8369, 82mtbiri 326 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ยฌ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 1 = 0))
84 fveq1 6890 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐‘โ€˜1) = ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜1))
85 fvpr1g 7187 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 โˆˆ V โˆง 1 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜1) = 1)
8632, 32, 34, 85mp3an 1461 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜1) = 1
8784, 86eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐‘โ€˜1) = 1)
8887oveq2d 7424 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐ด ยท (๐‘โ€˜1)) = (๐ด ยท 1))
89 fveq1 6890 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐‘โ€˜2) = ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜2))
90 ovex 7441 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (-๐ด / ๐ต) โˆˆ V
91 fvpr2g 7188 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 โˆˆ V โˆง (-๐ด / ๐ต) โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜2) = (-๐ด / ๐ต))
9240, 90, 34, 91mp3an 1461 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜2) = (-๐ด / ๐ต)
9389, 92eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐‘โ€˜2) = (-๐ด / ๐ต))
9493oveq2d 7424 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐ต ยท (๐‘โ€˜2)) = (๐ต ยท (-๐ด / ๐ต)))
9588, 94oveq12d 7426 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ ((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))))
9695eqeq1d 2734 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ))
9787eqeq1d 2734 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ ((๐‘โ€˜1) = 0 โ†” 1 = 0))
9896, 97bibi12d 345 . . . . . . . . . . . . . . . . . . . 20 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ ((((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†” (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 1 = 0)))
9998notbid 317 . . . . . . . . . . . . . . . . . . 19 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†” ยฌ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 1 = 0)))
10099rspcev 3612 . . . . . . . . . . . . . . . . . 18 (({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โˆˆ ๐‘ƒ โˆง ยฌ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 1 = 0)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
10164, 83, 100syl2anc 584 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
102101expcom 414 . . . . . . . . . . . . . . . 16 ((๐ต โ‰  0 โˆง ๐ถ = 0) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
103102ex 413 . . . . . . . . . . . . . . 15 (๐ต โ‰  0 โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
10456, 103sylbir 234 . . . . . . . . . . . . . 14 (ยฌ ๐ต = 0 โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
105 notnotb 314 . . . . . . . . . . . . . . 15 (๐ต = 0 โ†” ยฌ ยฌ ๐ต = 0)
106 nne 2944 . . . . . . . . . . . . . . . 16 (ยฌ ๐ด โ‰  0 โ†” ๐ด = 0)
107106bicomi 223 . . . . . . . . . . . . . . 15 (๐ด = 0 โ†” ยฌ ๐ด โ‰  0)
108 1re 11213 . . . . . . . . . . . . . . . . . . 19 1 โˆˆ โ„
1094, 5prelrrx2 47389 . . . . . . . . . . . . . . . . . . 19 ((1 โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โˆˆ ๐‘ƒ)
110108, 108, 109mp2an 690 . . . . . . . . . . . . . . . . . 18 {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โˆˆ ๐‘ƒ
111 oveq1 7415 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ด = 0 โ†’ (๐ด ยท 1) = (0 ยท 1))
112111adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ด ยท 1) = (0 ยท 1))
113 ax-1cn 11167 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 โˆˆ โ„‚
114113mul02i 11402 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ยท 1) = 0
115112, 114eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ด ยท 1) = 0)
116 oveq1 7415 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ต = 0 โ†’ (๐ต ยท 1) = (0 ยท 1))
117116adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ต ยท 1) = (0 ยท 1))
118117, 114eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ต ยท 1) = 0)
119115, 118oveq12d 7426 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ต = 0 โˆง ๐ด = 0) โ†’ ((๐ด ยท 1) + (๐ต ยท 1)) = (0 + 0))
120119, 23eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . 21 ((๐ต = 0 โˆง ๐ด = 0) โ†’ ((๐ด ยท 1) + (๐ต ยท 1)) = 0)
121 id 22 . . . . . . . . . . . . . . . . . . . . 21 (๐ถ = 0 โ†’ ๐ถ = 0)
122120, 121eqeqan12d 2746 . . . . . . . . . . . . . . . . . . . 20 (((๐ต = 0 โˆง ๐ด = 0) โˆง ๐ถ = 0) โ†’ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ†” 0 = 0))
123122bibi1d 343 . . . . . . . . . . . . . . . . . . 19 (((๐ต = 0 โˆง ๐ด = 0) โˆง ๐ถ = 0) โ†’ ((((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ†” 1 = 0) โ†” (0 = 0 โ†” 1 = 0)))
12469, 123mtbiri 326 . . . . . . . . . . . . . . . . . 18 (((๐ต = 0 โˆง ๐ด = 0) โˆง ๐ถ = 0) โ†’ ยฌ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ†” 1 = 0))
125 fveq1 6890 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘โ€˜1) = ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜1))
126 fvpr1g 7187 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 โˆˆ V โˆง 1 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜1) = 1)
12732, 32, 34, 126mp3an 1461 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜1) = 1
128125, 127eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘โ€˜1) = 1)
129128oveq2d 7424 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐ด ยท (๐‘โ€˜1)) = (๐ด ยท 1))
130 fveq1 6890 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘โ€˜2) = ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜2))
131 fvpr2g 7188 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 โˆˆ V โˆง 1 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜2) = 1)
13240, 32, 34, 131mp3an 1461 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜2) = 1
133130, 132eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘โ€˜2) = 1)
134133oveq2d 7424 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐ต ยท (๐‘โ€˜2)) = (๐ต ยท 1))
135129, 134oveq12d 7426 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ ((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ((๐ด ยท 1) + (๐ต ยท 1)))
136135eqeq1d 2734 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” ((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ))
137128eqeq1d 2734 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ ((๐‘โ€˜1) = 0 โ†” 1 = 0))
138136, 137bibi12d 345 . . . . . . . . . . . . . . . . . . . 20 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ ((((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†” (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ†” 1 = 0)))
139138notbid 317 . . . . . . . . . . . . . . . . . . 19 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†” ยฌ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ†” 1 = 0)))
140139rspcev 3612 . . . . . . . . . . . . . . . . . 18 (({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โˆˆ ๐‘ƒ โˆง ยฌ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ†” 1 = 0)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
141110, 124, 140sylancr 587 . . . . . . . . . . . . . . . . 17 (((๐ต = 0 โˆง ๐ด = 0) โˆง ๐ถ = 0) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
142141a1d 25 . . . . . . . . . . . . . . . 16 (((๐ต = 0 โˆง ๐ด = 0) โˆง ๐ถ = 0) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
143142ex 413 . . . . . . . . . . . . . . 15 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
144105, 107, 143syl2anbr 599 . . . . . . . . . . . . . 14 ((ยฌ ยฌ ๐ต = 0 โˆง ยฌ ๐ด โ‰  0) โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
145104, 144jaoi3 1059 . . . . . . . . . . . . 13 ((ยฌ ๐ต = 0 โˆจ ยฌ ๐ด โ‰  0) โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
146145orcoms 870 . . . . . . . . . . . 12 ((ยฌ ๐ด โ‰  0 โˆจ ยฌ ๐ต = 0) โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
14755, 146sylbi 216 . . . . . . . . . . 11 (ยฌ (๐ด โ‰  0 โˆง ๐ต = 0) โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
148147com12 32 . . . . . . . . . 10 (๐ถ = 0 โ†’ (ยฌ (๐ด โ‰  0 โˆง ๐ต = 0) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
14954, 148sylbir 234 . . . . . . . . 9 (ยฌ ยฌ ๐ถ = 0 โ†’ (ยฌ (๐ด โ‰  0 โˆง ๐ต = 0) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
150149imp 407 . . . . . . . 8 ((ยฌ ยฌ ๐ถ = 0 โˆง ยฌ (๐ด โ‰  0 โˆง ๐ต = 0)) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
15153, 150jaoi3 1059 . . . . . . 7 ((ยฌ ๐ถ = 0 โˆจ ยฌ (๐ด โ‰  0 โˆง ๐ต = 0)) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
152151orcoms 870 . . . . . 6 ((ยฌ (๐ด โ‰  0 โˆง ๐ต = 0) โˆจ ยฌ ๐ถ = 0) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
153152com12 32 . . . . 5 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ((ยฌ (๐ด โ‰  0 โˆง ๐ต = 0) โˆจ ยฌ ๐ถ = 0) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
1541, 153biimtrid 241 . . . 4 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (ยฌ ((๐ด โ‰  0 โˆง ๐ต = 0) โˆง ๐ถ = 0) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
155 rexnal 3100 . . . 4 (โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†” ยฌ โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
156154, 155imbitrdi 250 . . 3 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (ยฌ ((๐ด โ‰  0 โˆง ๐ต = 0) โˆง ๐ถ = 0) โ†’ ยฌ โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
157156con4d 115 . 2 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†’ ((๐ด โ‰  0 โˆง ๐ต = 0) โˆง ๐ถ = 0)))
158 df-3an 1089 . 2 ((๐ด โ‰  0 โˆง ๐ต = 0 โˆง ๐ถ = 0) โ†” ((๐ด โ‰  0 โˆง ๐ต = 0) โˆง ๐ถ = 0))
159157, 158syl6ibr 251 1 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†’ (๐ด โ‰  0 โˆง ๐ต = 0 โˆง ๐ถ = 0)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070  Vcvv 3474  {cpr 4630  โŸจcop 4634  โ€˜cfv 6543  (class class class)co 7408   โ†‘m cmap 8819  โ„‚cc 11107  โ„cr 11108  0cc0 11109  1c1 11110   + caddc 11112   ยท cmul 11114  -cneg 11444   / cdiv 11870  2c2 12266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8702  df-map 8821  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-2 12274
This theorem is referenced by:  line2y  47431
  Copyright terms: Public domain W3C validator