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 47526
Description: Lemma for line2y 47530. 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 979 . . . . 5 (ยฌ ((๐ด โ‰  0 โˆง ๐ต = 0) โˆง ๐ถ = 0) โ†” (ยฌ (๐ด โ‰  0 โˆง ๐ต = 0) โˆจ ยฌ ๐ถ = 0))
2 df-ne 2940 . . . . . . . . 9 (๐ถ โ‰  0 โ†” ยฌ ๐ถ = 0)
3 0re 11221 . . . . . . . . . . . 12 0 โˆˆ โ„
4 line2ylem.i . . . . . . . . . . . . 13 ๐ผ = {1, 2}
5 line2ylem.p . . . . . . . . . . . . 13 ๐‘ƒ = (โ„ โ†‘m ๐ผ)
64, 5prelrrx2 47488 . . . . . . . . . . . 12 ((0 โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โˆˆ ๐‘ƒ)
73, 3, 6mp2an 689 . . . . . . . . . . 11 {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โˆˆ ๐‘ƒ
8 eqneqall 2950 . . . . . . . . . . . . . . . 16 (๐ถ = 0 โ†’ (๐ถ โ‰  0 โ†’ ยฌ 0 = 0))
98com12 32 . . . . . . . . . . . . . . 15 (๐ถ โ‰  0 โ†’ (๐ถ = 0 โ†’ ยฌ 0 = 0))
10 eqid 2731 . . . . . . . . . . . . . . . 16 0 = 0
1110pm2.24i 150 . . . . . . . . . . . . . . 15 (ยฌ 0 = 0 โ†’ ๐ถ = 0)
129, 11impbid1 224 . . . . . . . . . . . . . 14 (๐ถ โ‰  0 โ†’ (๐ถ = 0 โ†” ยฌ 0 = 0))
1312adantl 481 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ (๐ถ = 0 โ†” ยฌ 0 = 0))
14 xor3 382 . . . . . . . . . . . . 13 (ยฌ (๐ถ = 0 โ†” 0 = 0) โ†” (๐ถ = 0 โ†” ยฌ 0 = 0))
1513, 14sylibr 233 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ ยฌ (๐ถ = 0 โ†” 0 = 0))
16 simp1 1135 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ๐ด โˆˆ โ„)
1716recnd 11247 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ๐ด โˆˆ โ„‚)
1817mul01d 11418 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท 0) = 0)
19 simp2 1136 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ๐ต โˆˆ โ„)
2019recnd 11247 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ๐ต โˆˆ โ„‚)
2120mul01d 11418 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต ยท 0) = 0)
2218, 21oveq12d 7430 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยท 0) + (๐ต ยท 0)) = (0 + 0))
23 00id 11394 . . . . . . . . . . . . . . . . 17 (0 + 0) = 0
2422, 23eqtrdi 2787 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยท 0) + (๐ต ยท 0)) = 0)
2524eqeq1d 2733 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = ๐ถ))
26 eqcom 2738 . . . . . . . . . . . . . . 15 (0 = ๐ถ โ†” ๐ถ = 0)
2725, 26bitrdi 286 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” ๐ถ = 0))
2827adantr 480 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” ๐ถ = 0))
2928bibi1d 342 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ ((((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = 0) โ†” (๐ถ = 0 โ†” 0 = 0)))
3015, 29mtbird 324 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ ยฌ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = 0))
31 fveq1 6891 . . . . . . . . . . . . . . . . . 18 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐‘โ€˜1) = ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜1))
32 1ex 11215 . . . . . . . . . . . . . . . . . . 19 1 โˆˆ V
33 c0ex 11213 . . . . . . . . . . . . . . . . . . 19 0 โˆˆ V
34 1ne2 12425 . . . . . . . . . . . . . . . . . . 19 1 โ‰  2
35 fvpr1g 7191 . . . . . . . . . . . . . . . . . . 19 ((1 โˆˆ V โˆง 0 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜1) = 0)
3632, 33, 34, 35mp3an 1460 . . . . . . . . . . . . . . . . . 18 ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜1) = 0
3731, 36eqtrdi 2787 . . . . . . . . . . . . . . . . 17 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐‘โ€˜1) = 0)
3837oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐ด ยท (๐‘โ€˜1)) = (๐ด ยท 0))
39 fveq1 6891 . . . . . . . . . . . . . . . . . 18 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐‘โ€˜2) = ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜2))
40 2ex 12294 . . . . . . . . . . . . . . . . . . 19 2 โˆˆ V
41 fvpr2g 7192 . . . . . . . . . . . . . . . . . . 19 ((2 โˆˆ V โˆง 0 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜2) = 0)
4240, 33, 34, 41mp3an 1460 . . . . . . . . . . . . . . . . . 18 ({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ}โ€˜2) = 0
4339, 42eqtrdi 2787 . . . . . . . . . . . . . . . . 17 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐‘โ€˜2) = 0)
4443oveq2d 7428 . . . . . . . . . . . . . . . 16 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (๐ต ยท (๐‘โ€˜2)) = (๐ต ยท 0))
4538, 44oveq12d 7430 . . . . . . . . . . . . . . 15 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ ((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ((๐ด ยท 0) + (๐ต ยท 0)))
4645eqeq1d 2733 . . . . . . . . . . . . . 14 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” ((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ))
4737eqeq1d 2733 . . . . . . . . . . . . . 14 (๐‘ = {โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โ†’ ((๐‘โ€˜1) = 0 โ†” 0 = 0))
4846, 47bibi12d 344 . . . . . . . . . . . . 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 3613 . . . . . . . . . . 11 (({โŸจ1, 0โŸฉ, โŸจ2, 0โŸฉ} โˆˆ ๐‘ƒ โˆง ยฌ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ†” 0 = 0)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
517, 30, 50sylancr 586 . . . . . . . . . 10 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง ๐ถ โ‰  0) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
5251expcom 413 . . . . . . . . 9 (๐ถ โ‰  0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
532, 52sylbir 234 . . . . . . . 8 (ยฌ ๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
54 notnotb 314 . . . . . . . . . 10 (๐ถ = 0 โ†” ยฌ ยฌ ๐ถ = 0)
55 ianor 979 . . . . . . . . . . . 12 (ยฌ (๐ด โ‰  0 โˆง ๐ต = 0) โ†” (ยฌ ๐ด โ‰  0 โˆจ ยฌ ๐ต = 0))
56 df-ne 2940 . . . . . . . . . . . . . . 15 (๐ต โ‰  0 โ†” ยฌ ๐ต = 0)
57 1red 11220 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ 1 โˆˆ โ„)
5816adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ด โˆˆ โ„)
5958renegcld 11646 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ -๐ด โˆˆ โ„)
6019adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ต โˆˆ โ„)
61 simprl 768 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ต โ‰  0)
6259, 60, 61redivcld 12047 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (-๐ด / ๐ต) โˆˆ โ„)
634, 5prelrrx2 47488 . . . . . . . . . . . . . . . . . . 19 ((1 โˆˆ โ„ โˆง (-๐ด / ๐ต) โˆˆ โ„) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โˆˆ ๐‘ƒ)
6457, 62, 63syl2anc 583 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โˆˆ ๐‘ƒ)
65 ax-1ne0 11182 . . . . . . . . . . . . . . . . . . . . . 22 1 โ‰  0
6665neii 2941 . . . . . . . . . . . . . . . . . . . . 21 ยฌ 1 = 0
6710, 662th 263 . . . . . . . . . . . . . . . . . . . 20 (0 = 0 โ†” ยฌ 1 = 0)
68 xor3 382 . . . . . . . . . . . . . . . . . . . 20 (ยฌ (0 = 0 โ†” 1 = 0) โ†” (0 = 0 โ†” ยฌ 1 = 0))
6967, 68mpbir 230 . . . . . . . . . . . . . . . . . . 19 ยฌ (0 = 0 โ†” 1 = 0)
7017mulridd 11236 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท 1) = ๐ด)
7170adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (๐ด ยท 1) = ๐ด)
7217negcld 11563 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ -๐ด โˆˆ โ„‚)
7372adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ -๐ด โˆˆ โ„‚)
7420adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ต โˆˆ โ„‚)
7573, 74, 61divcan2d 11997 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (๐ต ยท (-๐ด / ๐ต)) = -๐ด)
7671, 75oveq12d 7430 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = (๐ด + -๐ด))
7717negidd 11566 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด + -๐ด) = 0)
7877adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (๐ด + -๐ด) = 0)
7976, 78eqtrd 2771 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = 0)
80 simprr 770 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ๐ถ = 0)
8179, 80eqeq12d 2747 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 0 = 0))
8281bibi1d 342 . . . . . . . . . . . . . . . . . . 19 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ((((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 1 = 0) โ†” (0 = 0 โ†” 1 = 0)))
8369, 82mtbiri 326 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ ยฌ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 1 = 0))
84 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐‘โ€˜1) = ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜1))
85 fvpr1g 7191 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 โˆˆ V โˆง 1 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜1) = 1)
8632, 32, 34, 85mp3an 1460 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜1) = 1
8784, 86eqtrdi 2787 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐‘โ€˜1) = 1)
8887oveq2d 7428 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐ด ยท (๐‘โ€˜1)) = (๐ด ยท 1))
89 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐‘โ€˜2) = ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜2))
90 ovex 7445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (-๐ด / ๐ต) โˆˆ V
91 fvpr2g 7192 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 โˆˆ V โˆง (-๐ด / ๐ต) โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜2) = (-๐ด / ๐ต))
9240, 90, 34, 91mp3an 1460 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ}โ€˜2) = (-๐ด / ๐ต)
9389, 92eqtrdi 2787 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐‘โ€˜2) = (-๐ด / ๐ต))
9493oveq2d 7428 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (๐ต ยท (๐‘โ€˜2)) = (๐ต ยท (-๐ด / ๐ต)))
9588, 94oveq12d 7430 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ ((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))))
9695eqeq1d 2733 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ))
9787eqeq1d 2733 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โ†’ ((๐‘โ€˜1) = 0 โ†” 1 = 0))
9896, 97bibi12d 344 . . . . . . . . . . . . . . . . . . . 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 3613 . . . . . . . . . . . . . . . . . 18 (({โŸจ1, 1โŸฉ, โŸจ2, (-๐ด / ๐ต)โŸฉ} โˆˆ ๐‘ƒ โˆง ยฌ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ†” 1 = 0)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
10164, 83, 100syl2anc 583 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โˆง (๐ต โ‰  0 โˆง ๐ถ = 0)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
102101expcom 413 . . . . . . . . . . . . . . . 16 ((๐ต โ‰  0 โˆง ๐ถ = 0) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
103102ex 412 . . . . . . . . . . . . . . 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 2943 . . . . . . . . . . . . . . . 16 (ยฌ ๐ด โ‰  0 โ†” ๐ด = 0)
107106bicomi 223 . . . . . . . . . . . . . . 15 (๐ด = 0 โ†” ยฌ ๐ด โ‰  0)
108 1re 11219 . . . . . . . . . . . . . . . . . . 19 1 โˆˆ โ„
1094, 5prelrrx2 47488 . . . . . . . . . . . . . . . . . . 19 ((1 โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โˆˆ ๐‘ƒ)
110108, 108, 109mp2an 689 . . . . . . . . . . . . . . . . . 18 {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โˆˆ ๐‘ƒ
111 oveq1 7419 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ด = 0 โ†’ (๐ด ยท 1) = (0 ยท 1))
112111adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ด ยท 1) = (0 ยท 1))
113 ax-1cn 11171 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 โˆˆ โ„‚
114113mul02i 11408 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ยท 1) = 0
115112, 114eqtrdi 2787 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ด ยท 1) = 0)
116 oveq1 7419 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ต = 0 โ†’ (๐ต ยท 1) = (0 ยท 1))
117116adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ต ยท 1) = (0 ยท 1))
118117, 114eqtrdi 2787 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ต ยท 1) = 0)
119115, 118oveq12d 7430 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ต = 0 โˆง ๐ด = 0) โ†’ ((๐ด ยท 1) + (๐ต ยท 1)) = (0 + 0))
120119, 23eqtrdi 2787 . . . . . . . . . . . . . . . . . . . . 21 ((๐ต = 0 โˆง ๐ด = 0) โ†’ ((๐ด ยท 1) + (๐ต ยท 1)) = 0)
121 id 22 . . . . . . . . . . . . . . . . . . . . 21 (๐ถ = 0 โ†’ ๐ถ = 0)
122120, 121eqeqan12d 2745 . . . . . . . . . . . . . . . . . . . 20 (((๐ต = 0 โˆง ๐ด = 0) โˆง ๐ถ = 0) โ†’ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ†” 0 = 0))
123122bibi1d 342 . . . . . . . . . . . . . . . . . . 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 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘โ€˜1) = ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜1))
126 fvpr1g 7191 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 โˆˆ V โˆง 1 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜1) = 1)
12732, 32, 34, 126mp3an 1460 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜1) = 1
128125, 127eqtrdi 2787 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘โ€˜1) = 1)
129128oveq2d 7428 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐ด ยท (๐‘โ€˜1)) = (๐ด ยท 1))
130 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘โ€˜2) = ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜2))
131 fvpr2g 7192 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 โˆˆ V โˆง 1 โˆˆ V โˆง 1 โ‰  2) โ†’ ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜2) = 1)
13240, 32, 34, 131mp3an 1460 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ}โ€˜2) = 1
133130, 132eqtrdi 2787 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘โ€˜2) = 1)
134133oveq2d 7428 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐ต ยท (๐‘โ€˜2)) = (๐ต ยท 1))
135129, 134oveq12d 7430 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ ((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ((๐ด ยท 1) + (๐ต ยท 1)))
136135eqeq1d 2733 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” ((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ))
137128eqeq1d 2733 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ = {โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โ†’ ((๐‘โ€˜1) = 0 โ†” 1 = 0))
138136, 137bibi12d 344 . . . . . . . . . . . . . . . . . . . 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 3613 . . . . . . . . . . . . . . . . . 18 (({โŸจ1, 1โŸฉ, โŸจ2, 1โŸฉ} โˆˆ ๐‘ƒ โˆง ยฌ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ†” 1 = 0)) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
141110, 124, 140sylancr 586 . . . . . . . . . . . . . . . . 17 (((๐ต = 0 โˆง ๐ด = 0) โˆง ๐ถ = 0) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))
142141a1d 25 . . . . . . . . . . . . . . . 16 (((๐ต = 0 โˆง ๐ด = 0) โˆง ๐ถ = 0) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
143142ex 412 . . . . . . . . . . . . . . 15 ((๐ต = 0 โˆง ๐ด = 0) โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
144105, 107, 143syl2anbr 598 . . . . . . . . . . . . . 14 ((ยฌ ยฌ ๐ต = 0 โˆง ยฌ ๐ด โ‰  0) โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
145104, 144jaoi3 1058 . . . . . . . . . . . . 13 ((ยฌ ๐ต = 0 โˆจ ยฌ ๐ด โ‰  0) โ†’ (๐ถ = 0 โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0))))
146145orcoms 869 . . . . . . . . . . . 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 406 . . . . . . . 8 ((ยฌ ยฌ ๐ถ = 0 โˆง ยฌ (๐ด โ‰  0 โˆง ๐ต = 0)) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
15153, 150jaoi3 1058 . . . . . . 7 ((ยฌ ๐ถ = 0 โˆจ ยฌ (๐ด โ‰  0 โˆง ๐ต = 0)) โ†’ ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ โˆƒ๐‘ โˆˆ ๐‘ƒ ยฌ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0)))
152151orcoms 869 . . . . . 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 3099 . . . 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 1088 . 2 ((๐ด โ‰  0 โˆง ๐ต = 0 โˆง ๐ถ = 0) โ†” ((๐ด โ‰  0 โˆง ๐ต = 0) โˆง ๐ถ = 0))
159157, 158imbitrrdi 251 1 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (โˆ€๐‘ โˆˆ ๐‘ƒ (((๐ด ยท (๐‘โ€˜1)) + (๐ต ยท (๐‘โ€˜2))) = ๐ถ โ†” (๐‘โ€˜1) = 0) โ†’ (๐ด โ‰  0 โˆง ๐ต = 0 โˆง ๐ถ = 0)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆง w3a 1086   = wceq 1540   โˆˆ wcel 2105   โ‰  wne 2939  โˆ€wral 3060  โˆƒwrex 3069  Vcvv 3473  {cpr 4631  โŸจcop 4635  โ€˜cfv 6544  (class class class)co 7412   โ†‘m cmap 8823  โ„‚cc 11111  โ„cr 11112  0cc0 11113  1c1 11114   + caddc 11116   ยท cmul 11118  -cneg 11450   / cdiv 11876  2c2 12272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8706  df-map 8825  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-2 12280
This theorem is referenced by:  line2y  47530
  Copyright terms: Public domain W3C validator