HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  cdj3lem1 Structured version   Visualization version   GIF version

Theorem cdj3lem1 31725
Description: A property of "๐ด and ๐ต are completely disjoint subspaces." Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdj1.1 ๐ด โˆˆ Sโ„‹
cdj1.2 ๐ต โˆˆ Sโ„‹
Assertion
Ref Expression
cdj3lem1 (โˆƒ๐‘ฅ โˆˆ โ„ (0 < ๐‘ฅ โˆง โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง)))) โ†’ (๐ด โˆฉ ๐ต) = 0โ„‹)
Distinct variable groups:   ๐‘ฅ,๐‘ฆ,๐‘ง,๐ด   ๐‘ฅ,๐ต,๐‘ฆ,๐‘ง

Proof of Theorem cdj3lem1
Dummy variable ๐‘ค is distinct from all other variables.
StepHypRef Expression
1 elin 3964 . . . . . . . . . . . 12 (๐‘ค โˆˆ (๐ด โˆฉ ๐ต) โ†” (๐‘ค โˆˆ ๐ด โˆง ๐‘ค โˆˆ ๐ต))
2 cdj1.2 . . . . . . . . . . . . . 14 ๐ต โˆˆ Sโ„‹
3 neg1cn 12328 . . . . . . . . . . . . . 14 -1 โˆˆ โ„‚
4 shmulcl 30509 . . . . . . . . . . . . . 14 ((๐ต โˆˆ Sโ„‹ โˆง -1 โˆˆ โ„‚ โˆง ๐‘ค โˆˆ ๐ต) โ†’ (-1 ยทโ„Ž ๐‘ค) โˆˆ ๐ต)
52, 3, 4mp3an12 1451 . . . . . . . . . . . . 13 (๐‘ค โˆˆ ๐ต โ†’ (-1 ยทโ„Ž ๐‘ค) โˆˆ ๐ต)
65anim2i 617 . . . . . . . . . . . 12 ((๐‘ค โˆˆ ๐ด โˆง ๐‘ค โˆˆ ๐ต) โ†’ (๐‘ค โˆˆ ๐ด โˆง (-1 ยทโ„Ž ๐‘ค) โˆˆ ๐ต))
71, 6sylbi 216 . . . . . . . . . . 11 (๐‘ค โˆˆ (๐ด โˆฉ ๐ต) โ†’ (๐‘ค โˆˆ ๐ด โˆง (-1 ยทโ„Ž ๐‘ค) โˆˆ ๐ต))
8 fveq2 6891 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ค โ†’ (normโ„Žโ€˜๐‘ฆ) = (normโ„Žโ€˜๐‘ค))
98oveq1d 7426 . . . . . . . . . . . . 13 (๐‘ฆ = ๐‘ค โ†’ ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) = ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜๐‘ง)))
10 fvoveq1 7434 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ค โ†’ (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง)) = (normโ„Žโ€˜(๐‘ค +โ„Ž ๐‘ง)))
1110oveq2d 7427 . . . . . . . . . . . . 13 (๐‘ฆ = ๐‘ค โ†’ (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง))) = (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž ๐‘ง))))
129, 11breq12d 5161 . . . . . . . . . . . 12 (๐‘ฆ = ๐‘ค โ†’ (((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง))) โ†” ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž ๐‘ง)))))
13 fveq2 6891 . . . . . . . . . . . . . 14 (๐‘ง = (-1 ยทโ„Ž ๐‘ค) โ†’ (normโ„Žโ€˜๐‘ง) = (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค)))
1413oveq2d 7427 . . . . . . . . . . . . 13 (๐‘ง = (-1 ยทโ„Ž ๐‘ค) โ†’ ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜๐‘ง)) = ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))))
15 oveq2 7419 . . . . . . . . . . . . . . 15 (๐‘ง = (-1 ยทโ„Ž ๐‘ค) โ†’ (๐‘ค +โ„Ž ๐‘ง) = (๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค)))
1615fveq2d 6895 . . . . . . . . . . . . . 14 (๐‘ง = (-1 ยทโ„Ž ๐‘ค) โ†’ (normโ„Žโ€˜(๐‘ค +โ„Ž ๐‘ง)) = (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค))))
1716oveq2d 7427 . . . . . . . . . . . . 13 (๐‘ง = (-1 ยทโ„Ž ๐‘ค) โ†’ (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž ๐‘ง))) = (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค)))))
1814, 17breq12d 5161 . . . . . . . . . . . 12 (๐‘ง = (-1 ยทโ„Ž ๐‘ค) โ†’ (((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž ๐‘ง))) โ†” ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค))))))
1912, 18rspc2v 3622 . . . . . . . . . . 11 ((๐‘ค โˆˆ ๐ด โˆง (-1 ยทโ„Ž ๐‘ค) โˆˆ ๐ต) โ†’ (โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง))) โ†’ ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค))))))
207, 19syl 17 . . . . . . . . . 10 (๐‘ค โˆˆ (๐ด โˆฉ ๐ต) โ†’ (โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง))) โ†’ ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค))))))
2120adantl 482 . . . . . . . . 9 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ค โˆˆ (๐ด โˆฉ ๐ต)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง))) โ†’ ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค))))))
22 cdj1.1 . . . . . . . . . . . 12 ๐ด โˆˆ Sโ„‹
2322, 2shincli 30653 . . . . . . . . . . 11 (๐ด โˆฉ ๐ต) โˆˆ Sโ„‹
2423sheli 30505 . . . . . . . . . 10 (๐‘ค โˆˆ (๐ด โˆฉ ๐ต) โ†’ ๐‘ค โˆˆ โ„‹)
25 normneg 30435 . . . . . . . . . . . . . . 15 (๐‘ค โˆˆ โ„‹ โ†’ (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค)) = (normโ„Žโ€˜๐‘ค))
2625oveq2d 7427 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) = ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜๐‘ค)))
27 normcl 30416 . . . . . . . . . . . . . . . 16 (๐‘ค โˆˆ โ„‹ โ†’ (normโ„Žโ€˜๐‘ค) โˆˆ โ„)
2827recnd 11244 . . . . . . . . . . . . . . 15 (๐‘ค โˆˆ โ„‹ โ†’ (normโ„Žโ€˜๐‘ค) โˆˆ โ„‚)
29282timesd 12457 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ โ„‹ โ†’ (2 ยท (normโ„Žโ€˜๐‘ค)) = ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜๐‘ค)))
3026, 29eqtr4d 2775 . . . . . . . . . . . . 13 (๐‘ค โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) = (2 ยท (normโ„Žโ€˜๐‘ค)))
3130adantl 482 . . . . . . . . . . . 12 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ค โˆˆ โ„‹) โ†’ ((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) = (2 ยท (normโ„Žโ€˜๐‘ค)))
32 hvnegid 30318 . . . . . . . . . . . . . . . . 17 (๐‘ค โˆˆ โ„‹ โ†’ (๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค)) = 0โ„Ž)
3332fveq2d 6895 . . . . . . . . . . . . . . . 16 (๐‘ค โˆˆ โ„‹ โ†’ (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค))) = (normโ„Žโ€˜0โ„Ž))
34 norm0 30419 . . . . . . . . . . . . . . . 16 (normโ„Žโ€˜0โ„Ž) = 0
3533, 34eqtrdi 2788 . . . . . . . . . . . . . . 15 (๐‘ค โˆˆ โ„‹ โ†’ (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค))) = 0)
3635oveq2d 7427 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ โ„‹ โ†’ (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค)))) = (๐‘ฅ ยท 0))
37 recn 11202 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ โ„ โ†’ ๐‘ฅ โˆˆ โ„‚)
3837mul01d 11415 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ โ„ โ†’ (๐‘ฅ ยท 0) = 0)
3936, 38sylan9eqr 2794 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ค โˆˆ โ„‹) โ†’ (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค)))) = 0)
40 2t0e0 12383 . . . . . . . . . . . . 13 (2 ยท 0) = 0
4139, 40eqtr4di 2790 . . . . . . . . . . . 12 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ค โˆˆ โ„‹) โ†’ (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค)))) = (2 ยท 0))
4231, 41breq12d 5161 . . . . . . . . . . 11 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ค โˆˆ โ„‹) โ†’ (((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค)))) โ†” (2 ยท (normโ„Žโ€˜๐‘ค)) โ‰ค (2 ยท 0)))
43 0re 11218 . . . . . . . . . . . . . . 15 0 โˆˆ โ„
44 letri3 11301 . . . . . . . . . . . . . . 15 (((normโ„Žโ€˜๐‘ค) โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ ((normโ„Žโ€˜๐‘ค) = 0 โ†” ((normโ„Žโ€˜๐‘ค) โ‰ค 0 โˆง 0 โ‰ค (normโ„Žโ€˜๐‘ค))))
4527, 43, 44sylancl 586 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ค) = 0 โ†” ((normโ„Žโ€˜๐‘ค) โ‰ค 0 โˆง 0 โ‰ค (normโ„Žโ€˜๐‘ค))))
46 normge0 30417 . . . . . . . . . . . . . . 15 (๐‘ค โˆˆ โ„‹ โ†’ 0 โ‰ค (normโ„Žโ€˜๐‘ค))
4746biantrud 532 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ค) โ‰ค 0 โ†” ((normโ„Žโ€˜๐‘ค) โ‰ค 0 โˆง 0 โ‰ค (normโ„Žโ€˜๐‘ค))))
48 2re 12288 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„
49 2pos 12317 . . . . . . . . . . . . . . . . 17 0 < 2
5048, 49pm3.2i 471 . . . . . . . . . . . . . . . 16 (2 โˆˆ โ„ โˆง 0 < 2)
51 lemul2 12069 . . . . . . . . . . . . . . . 16 (((normโ„Žโ€˜๐‘ค) โˆˆ โ„ โˆง 0 โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((normโ„Žโ€˜๐‘ค) โ‰ค 0 โ†” (2 ยท (normโ„Žโ€˜๐‘ค)) โ‰ค (2 ยท 0)))
5243, 50, 51mp3an23 1453 . . . . . . . . . . . . . . 15 ((normโ„Žโ€˜๐‘ค) โˆˆ โ„ โ†’ ((normโ„Žโ€˜๐‘ค) โ‰ค 0 โ†” (2 ยท (normโ„Žโ€˜๐‘ค)) โ‰ค (2 ยท 0)))
5327, 52syl 17 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ค) โ‰ค 0 โ†” (2 ยท (normโ„Žโ€˜๐‘ค)) โ‰ค (2 ยท 0)))
5445, 47, 533bitr2rd 307 . . . . . . . . . . . . 13 (๐‘ค โˆˆ โ„‹ โ†’ ((2 ยท (normโ„Žโ€˜๐‘ค)) โ‰ค (2 ยท 0) โ†” (normโ„Žโ€˜๐‘ค) = 0))
55 norm-i 30420 . . . . . . . . . . . . 13 (๐‘ค โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ค) = 0 โ†” ๐‘ค = 0โ„Ž))
5654, 55bitrd 278 . . . . . . . . . . . 12 (๐‘ค โˆˆ โ„‹ โ†’ ((2 ยท (normโ„Žโ€˜๐‘ค)) โ‰ค (2 ยท 0) โ†” ๐‘ค = 0โ„Ž))
5756adantl 482 . . . . . . . . . . 11 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ค โˆˆ โ„‹) โ†’ ((2 ยท (normโ„Žโ€˜๐‘ค)) โ‰ค (2 ยท 0) โ†” ๐‘ค = 0โ„Ž))
5842, 57bitrd 278 . . . . . . . . . 10 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ค โˆˆ โ„‹) โ†’ (((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค)))) โ†” ๐‘ค = 0โ„Ž))
5924, 58sylan2 593 . . . . . . . . 9 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ค โˆˆ (๐ด โˆฉ ๐ต)) โ†’ (((normโ„Žโ€˜๐‘ค) + (normโ„Žโ€˜(-1 ยทโ„Ž ๐‘ค))) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ค +โ„Ž (-1 ยทโ„Ž ๐‘ค)))) โ†” ๐‘ค = 0โ„Ž))
6021, 59sylibd 238 . . . . . . . 8 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ค โˆˆ (๐ด โˆฉ ๐ต)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง))) โ†’ ๐‘ค = 0โ„Ž))
6160impancom 452 . . . . . . 7 ((๐‘ฅ โˆˆ โ„ โˆง โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง)))) โ†’ (๐‘ค โˆˆ (๐ด โˆฉ ๐ต) โ†’ ๐‘ค = 0โ„Ž))
62 elch0 30545 . . . . . . 7 (๐‘ค โˆˆ 0โ„‹ โ†” ๐‘ค = 0โ„Ž)
6361, 62imbitrrdi 251 . . . . . 6 ((๐‘ฅ โˆˆ โ„ โˆง โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง)))) โ†’ (๐‘ค โˆˆ (๐ด โˆฉ ๐ต) โ†’ ๐‘ค โˆˆ 0โ„‹))
6463ssrdv 3988 . . . . 5 ((๐‘ฅ โˆˆ โ„ โˆง โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง)))) โ†’ (๐ด โˆฉ ๐ต) โŠ† 0โ„‹)
6564ex 413 . . . 4 (๐‘ฅ โˆˆ โ„ โ†’ (โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง))) โ†’ (๐ด โˆฉ ๐ต) โŠ† 0โ„‹))
66 shle0 30733 . . . . 5 ((๐ด โˆฉ ๐ต) โˆˆ Sโ„‹ โ†’ ((๐ด โˆฉ ๐ต) โŠ† 0โ„‹ โ†” (๐ด โˆฉ ๐ต) = 0โ„‹))
6723, 66ax-mp 5 . . . 4 ((๐ด โˆฉ ๐ต) โŠ† 0โ„‹ โ†” (๐ด โˆฉ ๐ต) = 0โ„‹)
6865, 67imbitrdi 250 . . 3 (๐‘ฅ โˆˆ โ„ โ†’ (โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง))) โ†’ (๐ด โˆฉ ๐ต) = 0โ„‹))
6968adantld 491 . 2 (๐‘ฅ โˆˆ โ„ โ†’ ((0 < ๐‘ฅ โˆง โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง)))) โ†’ (๐ด โˆฉ ๐ต) = 0โ„‹))
7069rexlimiv 3148 1 (โˆƒ๐‘ฅ โˆˆ โ„ (0 < ๐‘ฅ โˆง โˆ€๐‘ฆ โˆˆ ๐ด โˆ€๐‘ง โˆˆ ๐ต ((normโ„Žโ€˜๐‘ฆ) + (normโ„Žโ€˜๐‘ง)) โ‰ค (๐‘ฅ ยท (normโ„Žโ€˜(๐‘ฆ +โ„Ž ๐‘ง)))) โ†’ (๐ด โˆฉ ๐ต) = 0โ„‹)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3061  โˆƒwrex 3070   โˆฉ cin 3947   โŠ† wss 3948   class class class wbr 5148  โ€˜cfv 6543  (class class class)co 7411  โ„‚cc 11110  โ„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   ยท cmul 11117   < clt 11250   โ‰ค cle 11251  -cneg 11447  2c2 12269   โ„‹chba 30210   +โ„Ž cva 30211   ยทโ„Ž csm 30212  normโ„Žcno 30214  0โ„Žc0v 30215   Sโ„‹ csh 30219  0โ„‹c0h 30226
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 7727  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  ax-pre-sup 11190  ax-hilex 30290  ax-hfvadd 30291  ax-hvcom 30292  ax-hv0cl 30294  ax-hvaddid 30295  ax-hfvmul 30296  ax-hvmulid 30297  ax-hvmulass 30298  ax-hvdistr1 30299  ax-hvdistr2 30300  ax-hvmul0 30301  ax-hfi 30370  ax-his1 30373  ax-his3 30375  ax-his4 30376
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-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  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-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  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 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-seq 13969  df-exp 14030  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-hnorm 30259  df-hvsub 30262  df-sh 30498  df-ch0 30544
This theorem is referenced by:  cdj3lem2b  31728  cdj3i  31732
  Copyright terms: Public domain W3C validator