Step |
Hyp |
Ref |
Expression |
1 |
|
atom1d |
โข ( ๐ด โ HAtoms โ โ ๐ฆ โ โ ( ๐ฆ โ 0โ โง ๐ด = ( span โ { ๐ฆ } ) ) ) |
2 |
|
atom1d |
โข ( ๐ต โ HAtoms โ โ ๐ง โ โ ( ๐ง โ 0โ โง ๐ต = ( span โ { ๐ง } ) ) ) |
3 |
|
reeanv |
โข ( โ ๐ฆ โ โ โ ๐ง โ โ ( ( ๐ฆ โ 0โ โง ๐ด = ( span โ { ๐ฆ } ) ) โง ( ๐ง โ 0โ โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( โ ๐ฆ โ โ ( ๐ฆ โ 0โ โง ๐ด = ( span โ { ๐ฆ } ) ) โง โ ๐ง โ โ ( ๐ง โ 0โ โง ๐ต = ( span โ { ๐ง } ) ) ) ) |
4 |
|
an4 |
โข ( ( ( ๐ฆ โ 0โ โง ๐ด = ( span โ { ๐ฆ } ) ) โง ( ๐ง โ 0โ โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) ) |
5 |
|
neeq1 |
โข ( ๐ด = ( span โ { ๐ฆ } ) โ ( ๐ด โ ๐ต โ ( span โ { ๐ฆ } ) โ ๐ต ) ) |
6 |
|
neeq2 |
โข ( ๐ต = ( span โ { ๐ง } ) โ ( ( span โ { ๐ฆ } ) โ ๐ต โ ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) ) |
7 |
5 6
|
sylan9bb |
โข ( ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) โ ( ๐ด โ ๐ต โ ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) ) |
8 |
7
|
adantl |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ๐ด โ ๐ต โ ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) ) |
9 |
|
hvaddcl |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ๐ฆ +โ ๐ง ) โ โ ) |
10 |
9
|
adantr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) โ ( ๐ฆ +โ ๐ง ) โ โ ) |
11 |
|
hvaddeq0 |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( ๐ฆ +โ ๐ง ) = 0โ โ ๐ฆ = ( - 1 ยทโ ๐ง ) ) ) |
12 |
|
sneq |
โข ( ๐ฆ = ( - 1 ยทโ ๐ง ) โ { ๐ฆ } = { ( - 1 ยทโ ๐ง ) } ) |
13 |
12
|
fveq2d |
โข ( ๐ฆ = ( - 1 ยทโ ๐ง ) โ ( span โ { ๐ฆ } ) = ( span โ { ( - 1 ยทโ ๐ง ) } ) ) |
14 |
|
neg1cn |
โข - 1 โ โ |
15 |
|
neg1ne0 |
โข - 1 โ 0 |
16 |
|
spansncol |
โข ( ( ๐ง โ โ โง - 1 โ โ โง - 1 โ 0 ) โ ( span โ { ( - 1 ยทโ ๐ง ) } ) = ( span โ { ๐ง } ) ) |
17 |
14 15 16
|
mp3an23 |
โข ( ๐ง โ โ โ ( span โ { ( - 1 ยทโ ๐ง ) } ) = ( span โ { ๐ง } ) ) |
18 |
13 17
|
sylan9eqr |
โข ( ( ๐ง โ โ โง ๐ฆ = ( - 1 ยทโ ๐ง ) ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) |
19 |
18
|
ex |
โข ( ๐ง โ โ โ ( ๐ฆ = ( - 1 ยทโ ๐ง ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
20 |
19
|
adantl |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ๐ฆ = ( - 1 ยทโ ๐ง ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
21 |
11 20
|
sylbid |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( ๐ฆ +โ ๐ง ) = 0โ โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
22 |
21
|
necon3d |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) โ ( ๐ฆ +โ ๐ง ) โ 0โ ) ) |
23 |
22
|
imp |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) โ ( ๐ฆ +โ ๐ง ) โ 0โ ) |
24 |
|
spansna |
โข ( ( ( ๐ฆ +โ ๐ง ) โ โ โง ( ๐ฆ +โ ๐ง ) โ 0โ ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ HAtoms ) |
25 |
10 23 24
|
syl2anc |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ HAtoms ) |
26 |
25
|
adantlr |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ HAtoms ) |
27 |
26
|
adantlr |
โข ( ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โง ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ HAtoms ) |
28 |
|
eqeq2 |
โข ( ๐ด = ( span โ { ๐ฆ } ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ๐ด โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ฆ } ) ) ) |
29 |
28
|
biimpd |
โข ( ๐ด = ( span โ { ๐ฆ } ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ๐ด โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ฆ } ) ) ) |
30 |
|
spansneleqi |
โข ( ( ๐ฆ +โ ๐ง ) โ โ โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ฆ } ) โ ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ฆ } ) ) ) |
31 |
9 30
|
syl |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ฆ } ) โ ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ฆ } ) ) ) |
32 |
|
elspansn |
โข ( ๐ฆ โ โ โ ( ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ฆ } ) โ โ ๐ฃ โ โ ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) ) ) |
33 |
32
|
adantr |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ฆ } ) โ โ ๐ฃ โ โ ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) ) ) |
34 |
|
addcl |
โข ( ( ๐ฃ โ โ โง - 1 โ โ ) โ ( ๐ฃ + - 1 ) โ โ ) |
35 |
14 34
|
mpan2 |
โข ( ๐ฃ โ โ โ ( ๐ฃ + - 1 ) โ โ ) |
36 |
35
|
ad2antlr |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) ) โ ( ๐ฃ + - 1 ) โ โ ) |
37 |
|
hvmulcl |
โข ( ( ๐ฃ โ โ โง ๐ฆ โ โ ) โ ( ๐ฃ ยทโ ๐ฆ ) โ โ ) |
38 |
37
|
ancoms |
โข ( ( ๐ฆ โ โ โง ๐ฃ โ โ ) โ ( ๐ฃ ยทโ ๐ฆ ) โ โ ) |
39 |
38
|
adantlr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ( ๐ฃ ยทโ ๐ฆ ) โ โ ) |
40 |
|
simpll |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ๐ฆ โ โ ) |
41 |
|
simplr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ๐ง โ โ ) |
42 |
|
hvsubadd |
โข ( ( ( ๐ฃ ยทโ ๐ฆ ) โ โ โง ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( ( ๐ฃ ยทโ ๐ฆ ) โโ ๐ฆ ) = ๐ง โ ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) ) ) |
43 |
39 40 41 42
|
syl3anc |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ( ( ( ๐ฃ ยทโ ๐ฆ ) โโ ๐ฆ ) = ๐ง โ ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) ) ) |
44 |
43
|
biimpar |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) ) โ ( ( ๐ฃ ยทโ ๐ฆ ) โโ ๐ฆ ) = ๐ง ) |
45 |
|
hvsubval |
โข ( ( ( ๐ฃ ยทโ ๐ฆ ) โ โ โง ๐ฆ โ โ ) โ ( ( ๐ฃ ยทโ ๐ฆ ) โโ ๐ฆ ) = ( ( ๐ฃ ยทโ ๐ฆ ) +โ ( - 1 ยทโ ๐ฆ ) ) ) |
46 |
37 45
|
sylancom |
โข ( ( ๐ฃ โ โ โง ๐ฆ โ โ ) โ ( ( ๐ฃ ยทโ ๐ฆ ) โโ ๐ฆ ) = ( ( ๐ฃ ยทโ ๐ฆ ) +โ ( - 1 ยทโ ๐ฆ ) ) ) |
47 |
|
ax-hvdistr2 |
โข ( ( ๐ฃ โ โ โง - 1 โ โ โง ๐ฆ โ โ ) โ ( ( ๐ฃ + - 1 ) ยทโ ๐ฆ ) = ( ( ๐ฃ ยทโ ๐ฆ ) +โ ( - 1 ยทโ ๐ฆ ) ) ) |
48 |
14 47
|
mp3an2 |
โข ( ( ๐ฃ โ โ โง ๐ฆ โ โ ) โ ( ( ๐ฃ + - 1 ) ยทโ ๐ฆ ) = ( ( ๐ฃ ยทโ ๐ฆ ) +โ ( - 1 ยทโ ๐ฆ ) ) ) |
49 |
46 48
|
eqtr4d |
โข ( ( ๐ฃ โ โ โง ๐ฆ โ โ ) โ ( ( ๐ฃ ยทโ ๐ฆ ) โโ ๐ฆ ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ฆ ) ) |
50 |
49
|
ancoms |
โข ( ( ๐ฆ โ โ โง ๐ฃ โ โ ) โ ( ( ๐ฃ ยทโ ๐ฆ ) โโ ๐ฆ ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ฆ ) ) |
51 |
50
|
adantlr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ( ( ๐ฃ ยทโ ๐ฆ ) โโ ๐ฆ ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ฆ ) ) |
52 |
51
|
adantr |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) ) โ ( ( ๐ฃ ยทโ ๐ฆ ) โโ ๐ฆ ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ฆ ) ) |
53 |
44 52
|
eqtr3d |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) ) โ ๐ง = ( ( ๐ฃ + - 1 ) ยทโ ๐ฆ ) ) |
54 |
|
oveq1 |
โข ( ๐ค = ( ๐ฃ + - 1 ) โ ( ๐ค ยทโ ๐ฆ ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ฆ ) ) |
55 |
54
|
rspceeqv |
โข ( ( ( ๐ฃ + - 1 ) โ โ โง ๐ง = ( ( ๐ฃ + - 1 ) ยทโ ๐ฆ ) ) โ โ ๐ค โ โ ๐ง = ( ๐ค ยทโ ๐ฆ ) ) |
56 |
36 53 55
|
syl2anc |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) ) โ โ ๐ค โ โ ๐ง = ( ๐ค ยทโ ๐ฆ ) ) |
57 |
56
|
rexlimdva2 |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( โ ๐ฃ โ โ ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ฆ ) โ โ ๐ค โ โ ๐ง = ( ๐ค ยทโ ๐ฆ ) ) ) |
58 |
33 57
|
sylbid |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ฆ } ) โ โ ๐ค โ โ ๐ง = ( ๐ค ยทโ ๐ฆ ) ) ) |
59 |
31 58
|
syld |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ฆ } ) โ โ ๐ค โ โ ๐ง = ( ๐ค ยทโ ๐ฆ ) ) ) |
60 |
|
elspansn |
โข ( ๐ฆ โ โ โ ( ๐ง โ ( span โ { ๐ฆ } ) โ โ ๐ค โ โ ๐ง = ( ๐ค ยทโ ๐ฆ ) ) ) |
61 |
60
|
adantr |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ๐ง โ ( span โ { ๐ฆ } ) โ โ ๐ค โ โ ๐ง = ( ๐ค ยทโ ๐ฆ ) ) ) |
62 |
59 61
|
sylibrd |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ฆ } ) โ ๐ง โ ( span โ { ๐ฆ } ) ) ) |
63 |
62
|
adantr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ง โ 0โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ฆ } ) โ ๐ง โ ( span โ { ๐ฆ } ) ) ) |
64 |
|
spansneleq |
โข ( ( ๐ฆ โ โ โง ๐ง โ 0โ ) โ ( ๐ง โ ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) = ( span โ { ๐ฆ } ) ) ) |
65 |
|
eqcom |
โข ( ( span โ { ๐ง } ) = ( span โ { ๐ฆ } ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) |
66 |
64 65
|
syl6ib |
โข ( ( ๐ฆ โ โ โง ๐ง โ 0โ ) โ ( ๐ง โ ( span โ { ๐ฆ } ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
67 |
66
|
adantlr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ง โ 0โ ) โ ( ๐ง โ ( span โ { ๐ฆ } ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
68 |
63 67
|
syld |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ง โ 0โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ฆ } ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
69 |
29 68
|
sylan9r |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ง โ 0โ ) โง ๐ด = ( span โ { ๐ฆ } ) ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ๐ด โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
70 |
69
|
necon3d |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ง โ 0โ ) โง ๐ด = ( span โ { ๐ฆ } ) ) โ ( ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ด ) ) |
71 |
70
|
adantlrl |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ๐ด = ( span โ { ๐ฆ } ) ) โ ( ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ด ) ) |
72 |
71
|
adantrr |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ด ) ) |
73 |
72
|
imp |
โข ( ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โง ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ด ) |
74 |
|
eqeq2 |
โข ( ๐ต = ( span โ { ๐ง } ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ๐ต โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ง } ) ) ) |
75 |
74
|
biimpd |
โข ( ๐ต = ( span โ { ๐ง } ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ๐ต โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ง } ) ) ) |
76 |
|
spansneleqi |
โข ( ( ๐ฆ +โ ๐ง ) โ โ โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ง } ) โ ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ง } ) ) ) |
77 |
9 76
|
syl |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ง } ) โ ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ง } ) ) ) |
78 |
|
elspansn |
โข ( ๐ง โ โ โ ( ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ง } ) โ โ ๐ฃ โ โ ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) ) ) |
79 |
78
|
adantl |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ง } ) โ โ ๐ฃ โ โ ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) ) ) |
80 |
35
|
ad2antlr |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) ) โ ( ๐ฃ + - 1 ) โ โ ) |
81 |
|
hvmulcl |
โข ( ( ๐ฃ โ โ โง ๐ง โ โ ) โ ( ๐ฃ ยทโ ๐ง ) โ โ ) |
82 |
81
|
ancoms |
โข ( ( ๐ง โ โ โง ๐ฃ โ โ ) โ ( ๐ฃ ยทโ ๐ง ) โ โ ) |
83 |
82
|
adantll |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ( ๐ฃ ยทโ ๐ง ) โ โ ) |
84 |
|
hvsubadd |
โข ( ( ( ๐ฃ ยทโ ๐ง ) โ โ โง ๐ง โ โ โง ๐ฆ โ โ ) โ ( ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ๐ฆ โ ( ๐ง +โ ๐ฆ ) = ( ๐ฃ ยทโ ๐ง ) ) ) |
85 |
83 41 40 84
|
syl3anc |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ( ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ๐ฆ โ ( ๐ง +โ ๐ฆ ) = ( ๐ฃ ยทโ ๐ง ) ) ) |
86 |
|
ax-hvcom |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ๐ฆ +โ ๐ง ) = ( ๐ง +โ ๐ฆ ) ) |
87 |
86
|
adantr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ( ๐ฆ +โ ๐ง ) = ( ๐ง +โ ๐ฆ ) ) |
88 |
87
|
eqeq1d |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ( ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) โ ( ๐ง +โ ๐ฆ ) = ( ๐ฃ ยทโ ๐ง ) ) ) |
89 |
85 88
|
bitr4d |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ( ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ๐ฆ โ ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) ) ) |
90 |
89
|
biimpar |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) ) โ ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ๐ฆ ) |
91 |
|
hvsubval |
โข ( ( ( ๐ฃ ยทโ ๐ง ) โ โ โง ๐ง โ โ ) โ ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ( ( ๐ฃ ยทโ ๐ง ) +โ ( - 1 ยทโ ๐ง ) ) ) |
92 |
81 91
|
sylancom |
โข ( ( ๐ฃ โ โ โง ๐ง โ โ ) โ ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ( ( ๐ฃ ยทโ ๐ง ) +โ ( - 1 ยทโ ๐ง ) ) ) |
93 |
|
ax-hvdistr2 |
โข ( ( ๐ฃ โ โ โง - 1 โ โ โง ๐ง โ โ ) โ ( ( ๐ฃ + - 1 ) ยทโ ๐ง ) = ( ( ๐ฃ ยทโ ๐ง ) +โ ( - 1 ยทโ ๐ง ) ) ) |
94 |
14 93
|
mp3an2 |
โข ( ( ๐ฃ โ โ โง ๐ง โ โ ) โ ( ( ๐ฃ + - 1 ) ยทโ ๐ง ) = ( ( ๐ฃ ยทโ ๐ง ) +โ ( - 1 ยทโ ๐ง ) ) ) |
95 |
92 94
|
eqtr4d |
โข ( ( ๐ฃ โ โ โง ๐ง โ โ ) โ ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ง ) ) |
96 |
95
|
ancoms |
โข ( ( ๐ง โ โ โง ๐ฃ โ โ ) โ ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ง ) ) |
97 |
96
|
adantll |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โ ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ง ) ) |
98 |
97
|
adantr |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) ) โ ( ( ๐ฃ ยทโ ๐ง ) โโ ๐ง ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ง ) ) |
99 |
90 98
|
eqtr3d |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) ) โ ๐ฆ = ( ( ๐ฃ + - 1 ) ยทโ ๐ง ) ) |
100 |
|
oveq1 |
โข ( ๐ค = ( ๐ฃ + - 1 ) โ ( ๐ค ยทโ ๐ง ) = ( ( ๐ฃ + - 1 ) ยทโ ๐ง ) ) |
101 |
100
|
rspceeqv |
โข ( ( ( ๐ฃ + - 1 ) โ โ โง ๐ฆ = ( ( ๐ฃ + - 1 ) ยทโ ๐ง ) ) โ โ ๐ค โ โ ๐ฆ = ( ๐ค ยทโ ๐ง ) ) |
102 |
80 99 101
|
syl2anc |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฃ โ โ ) โง ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) ) โ โ ๐ค โ โ ๐ฆ = ( ๐ค ยทโ ๐ง ) ) |
103 |
102
|
rexlimdva2 |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( โ ๐ฃ โ โ ( ๐ฆ +โ ๐ง ) = ( ๐ฃ ยทโ ๐ง ) โ โ ๐ค โ โ ๐ฆ = ( ๐ค ยทโ ๐ง ) ) ) |
104 |
79 103
|
sylbid |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( ๐ฆ +โ ๐ง ) โ ( span โ { ๐ง } ) โ โ ๐ค โ โ ๐ฆ = ( ๐ค ยทโ ๐ง ) ) ) |
105 |
77 104
|
syld |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ง } ) โ โ ๐ค โ โ ๐ฆ = ( ๐ค ยทโ ๐ง ) ) ) |
106 |
|
elspansn |
โข ( ๐ง โ โ โ ( ๐ฆ โ ( span โ { ๐ง } ) โ โ ๐ค โ โ ๐ฆ = ( ๐ค ยทโ ๐ง ) ) ) |
107 |
106
|
adantl |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ๐ฆ โ ( span โ { ๐ง } ) โ โ ๐ค โ โ ๐ฆ = ( ๐ค ยทโ ๐ง ) ) ) |
108 |
105 107
|
sylibrd |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ง } ) โ ๐ฆ โ ( span โ { ๐ง } ) ) ) |
109 |
108
|
adantr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฆ โ 0โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ง } ) โ ๐ฆ โ ( span โ { ๐ง } ) ) ) |
110 |
|
spansneleq |
โข ( ( ๐ง โ โ โง ๐ฆ โ 0โ ) โ ( ๐ฆ โ ( span โ { ๐ง } ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
111 |
110
|
adantll |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฆ โ 0โ ) โ ( ๐ฆ โ ( span โ { ๐ง } ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
112 |
109 111
|
syld |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฆ โ 0โ ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ( span โ { ๐ง } ) โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
113 |
75 112
|
sylan9r |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฆ โ 0โ ) โง ๐ต = ( span โ { ๐ง } ) ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) = ๐ต โ ( span โ { ๐ฆ } ) = ( span โ { ๐ง } ) ) ) |
114 |
113
|
necon3d |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ๐ฆ โ 0โ ) โง ๐ต = ( span โ { ๐ง } ) ) โ ( ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ต ) ) |
115 |
114
|
adantlrr |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ๐ต = ( span โ { ๐ง } ) ) โ ( ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ต ) ) |
116 |
115
|
adantrl |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ต ) ) |
117 |
116
|
imp |
โข ( ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โง ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ต ) |
118 |
|
spanpr |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( span โ { ๐ฆ , ๐ง } ) ) |
119 |
118
|
adantr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( span โ { ๐ฆ , ๐ง } ) ) |
120 |
|
oveq12 |
โข ( ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) โ ( ๐ด โจโ ๐ต ) = ( ( span โ { ๐ฆ } ) โจโ ( span โ { ๐ง } ) ) ) |
121 |
|
df-pr |
โข { ๐ฆ , ๐ง } = ( { ๐ฆ } โช { ๐ง } ) |
122 |
121
|
fveq2i |
โข ( span โ { ๐ฆ , ๐ง } ) = ( span โ ( { ๐ฆ } โช { ๐ง } ) ) |
123 |
|
snssi |
โข ( ๐ฆ โ โ โ { ๐ฆ } โ โ ) |
124 |
|
snssi |
โข ( ๐ง โ โ โ { ๐ง } โ โ ) |
125 |
|
spanun |
โข ( ( { ๐ฆ } โ โ โง { ๐ง } โ โ ) โ ( span โ ( { ๐ฆ } โช { ๐ง } ) ) = ( ( span โ { ๐ฆ } ) +โ ( span โ { ๐ง } ) ) ) |
126 |
123 124 125
|
syl2an |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( span โ ( { ๐ฆ } โช { ๐ง } ) ) = ( ( span โ { ๐ฆ } ) +โ ( span โ { ๐ง } ) ) ) |
127 |
122 126
|
eqtrid |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( span โ { ๐ฆ , ๐ง } ) = ( ( span โ { ๐ฆ } ) +โ ( span โ { ๐ง } ) ) ) |
128 |
|
spansnch |
โข ( ๐ฆ โ โ โ ( span โ { ๐ฆ } ) โ Cโ ) |
129 |
|
spansnj |
โข ( ( ( span โ { ๐ฆ } ) โ Cโ โง ๐ง โ โ ) โ ( ( span โ { ๐ฆ } ) +โ ( span โ { ๐ง } ) ) = ( ( span โ { ๐ฆ } ) โจโ ( span โ { ๐ง } ) ) ) |
130 |
128 129
|
sylan |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( span โ { ๐ฆ } ) +โ ( span โ { ๐ง } ) ) = ( ( span โ { ๐ฆ } ) โจโ ( span โ { ๐ง } ) ) ) |
131 |
127 130
|
eqtr2d |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( span โ { ๐ฆ } ) โจโ ( span โ { ๐ง } ) ) = ( span โ { ๐ฆ , ๐ง } ) ) |
132 |
120 131
|
sylan9eqr |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ๐ด โจโ ๐ต ) = ( span โ { ๐ฆ , ๐ง } ) ) |
133 |
119 132
|
sseqtrrd |
โข ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ๐ด โจโ ๐ต ) ) |
134 |
133
|
adantlr |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ๐ด โจโ ๐ต ) ) |
135 |
134
|
adantr |
โข ( ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โง ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ๐ด โจโ ๐ต ) ) |
136 |
|
neeq1 |
โข ( ๐ฅ = ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ๐ฅ โ ๐ด โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ด ) ) |
137 |
|
neeq1 |
โข ( ๐ฅ = ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ๐ฅ โ ๐ต โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ต ) ) |
138 |
|
sseq1 |
โข ( ๐ฅ = ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ๐ฅ โ ( ๐ด โจโ ๐ต ) โ ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ๐ด โจโ ๐ต ) ) ) |
139 |
136 137 138
|
3anbi123d |
โข ( ๐ฅ = ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) โ ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ด โง ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ต โง ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ๐ด โจโ ๐ต ) ) ) ) |
140 |
139
|
rspcev |
โข ( ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ HAtoms โง ( ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ด โง ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ๐ต โง ( span โ { ( ๐ฆ +โ ๐ง ) } ) โ ( ๐ด โจโ ๐ต ) ) ) โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) |
141 |
27 73 117 135 140
|
syl13anc |
โข ( ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โง ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) ) โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) |
142 |
141
|
ex |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ( span โ { ๐ฆ } ) โ ( span โ { ๐ง } ) โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) ) |
143 |
8 142
|
sylbid |
โข ( ( ( ( ๐ฆ โ โ โง ๐ง โ โ ) โง ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ๐ด โ ๐ต โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) ) |
144 |
143
|
expl |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( ( ๐ฆ โ 0โ โง ๐ง โ 0โ ) โง ( ๐ด = ( span โ { ๐ฆ } ) โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ๐ด โ ๐ต โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) ) ) |
145 |
4 144
|
syl5bi |
โข ( ( ๐ฆ โ โ โง ๐ง โ โ ) โ ( ( ( ๐ฆ โ 0โ โง ๐ด = ( span โ { ๐ฆ } ) ) โง ( ๐ง โ 0โ โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ๐ด โ ๐ต โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) ) ) |
146 |
145
|
rexlimivv |
โข ( โ ๐ฆ โ โ โ ๐ง โ โ ( ( ๐ฆ โ 0โ โง ๐ด = ( span โ { ๐ฆ } ) ) โง ( ๐ง โ 0โ โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ๐ด โ ๐ต โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) ) |
147 |
3 146
|
sylbir |
โข ( ( โ ๐ฆ โ โ ( ๐ฆ โ 0โ โง ๐ด = ( span โ { ๐ฆ } ) ) โง โ ๐ง โ โ ( ๐ง โ 0โ โง ๐ต = ( span โ { ๐ง } ) ) ) โ ( ๐ด โ ๐ต โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) ) |
148 |
1 2 147
|
syl2anb |
โข ( ( ๐ด โ HAtoms โง ๐ต โ HAtoms ) โ ( ๐ด โ ๐ต โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) ) |
149 |
148
|
3impia |
โข ( ( ๐ด โ HAtoms โง ๐ต โ HAtoms โง ๐ด โ ๐ต ) โ โ ๐ฅ โ HAtoms ( ๐ฅ โ ๐ด โง ๐ฅ โ ๐ต โง ๐ฅ โ ( ๐ด โจโ ๐ต ) ) ) |