Step | Hyp | Ref
| Expression |
1 | | mulcl 11142 |
. . . . . . . . 9
β’ ((π¦ β β β§ π΅ β β) β (π¦ Β· π΅) β β) |
2 | 1 | ancoms 460 |
. . . . . . . 8
β’ ((π΅ β β β§ π¦ β β) β (π¦ Β· π΅) β β) |
3 | 2 | adantll 713 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β) β§ π¦ β β) β (π¦ Β· π΅) β β) |
4 | | ax-hvmulass 29991 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ π΅ β β β§ π΄ β β) β ((π¦ Β· π΅) Β·β π΄) = (π¦ Β·β (π΅
Β·β π΄))) |
5 | 4 | 3com13 1125 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β β§ π¦ β β) β ((π¦ Β· π΅) Β·β π΄) = (π¦ Β·β (π΅
Β·β π΄))) |
6 | 5 | 3expa 1119 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β) β§ π¦ β β) β ((π¦ Β· π΅) Β·β π΄) = (π¦ Β·β (π΅
Β·β π΄))) |
7 | 6 | eqeq2d 2748 |
. . . . . . . 8
β’ (((π΄ β β β§ π΅ β β) β§ π¦ β β) β (π₯ = ((π¦ Β· π΅) Β·β π΄) β π₯ = (π¦ Β·β (π΅
Β·β π΄)))) |
8 | 7 | biimprd 248 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β) β§ π¦ β β) β (π₯ = (π¦ Β·β (π΅
Β·β π΄)) β π₯ = ((π¦ Β· π΅) Β·β π΄))) |
9 | | oveq1 7369 |
. . . . . . . 8
β’ (π§ = (π¦ Β· π΅) β (π§ Β·β π΄) = ((π¦ Β· π΅) Β·β π΄)) |
10 | 9 | rspceeqv 3600 |
. . . . . . 7
β’ (((π¦ Β· π΅) β β β§ π₯ = ((π¦ Β· π΅) Β·β π΄)) β βπ§ β β π₯ = (π§ Β·β π΄)) |
11 | 3, 8, 10 | syl6an 683 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β) β§ π¦ β β) β (π₯ = (π¦ Β·β (π΅
Β·β π΄)) β βπ§ β β π₯ = (π§ Β·β π΄))) |
12 | 11 | rexlimdva 3153 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
(βπ¦ β β
π₯ = (π¦ Β·β (π΅
Β·β π΄)) β βπ§ β β π₯ = (π§ Β·β π΄))) |
13 | 12 | 3adant3 1133 |
. . . 4
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄)) β βπ§ β β π₯ = (π§ Β·β π΄))) |
14 | | divcl 11826 |
. . . . . . . . . . 11
β’ ((π§ β β β§ π΅ β β β§ π΅ β 0) β (π§ / π΅) β β) |
15 | 14 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π§ β β β§ (π΅ β β β§ π΅ β 0)) β (π§ / π΅) β β) |
16 | 15 | adantlr 714 |
. . . . . . . . 9
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β (π§ / π΅) β β) |
17 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β π΅ β
β) |
18 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β π΄ β
β) |
19 | | ax-hvmulass 29991 |
. . . . . . . . . . . . 13
β’ (((π§ / π΅) β β β§ π΅ β β β§ π΄ β β) β (((π§ / π΅) Β· π΅) Β·β π΄) = ((π§ / π΅) Β·β (π΅
Β·β π΄))) |
20 | 16, 17, 18, 19 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β (((π§ / π΅) Β· π΅) Β·β π΄) = ((π§ / π΅) Β·β (π΅
Β·β π΄))) |
21 | | divcan1 11829 |
. . . . . . . . . . . . . . 15
β’ ((π§ β β β§ π΅ β β β§ π΅ β 0) β ((π§ / π΅) Β· π΅) = π§) |
22 | 21 | 3expb 1121 |
. . . . . . . . . . . . . 14
β’ ((π§ β β β§ (π΅ β β β§ π΅ β 0)) β ((π§ / π΅) Β· π΅) = π§) |
23 | 22 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β ((π§ / π΅) Β· π΅) = π§) |
24 | 23 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β (((π§ / π΅) Β· π΅) Β·β π΄) = (π§ Β·β π΄)) |
25 | 20, 24 | eqtr3d 2779 |
. . . . . . . . . . 11
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β ((π§ / π΅) Β·β (π΅
Β·β π΄)) = (π§ Β·β π΄)) |
26 | 25 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β (π₯ = ((π§ / π΅) Β·β (π΅
Β·β π΄)) β π₯ = (π§ Β·β π΄))) |
27 | 26 | biimprd 248 |
. . . . . . . . 9
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β (π₯ = (π§ Β·β π΄) β π₯ = ((π§ / π΅) Β·β (π΅
Β·β π΄)))) |
28 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π¦ = (π§ / π΅) β (π¦ Β·β (π΅
Β·β π΄)) = ((π§ / π΅) Β·β (π΅
Β·β π΄))) |
29 | 28 | rspceeqv 3600 |
. . . . . . . . 9
β’ (((π§ / π΅) β β β§ π₯ = ((π§ / π΅) Β·β (π΅
Β·β π΄))) β βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄))) |
30 | 16, 27, 29 | syl6an 683 |
. . . . . . . 8
β’ (((π§ β β β§ π΄ β β) β§ (π΅ β β β§ π΅ β 0)) β (π₯ = (π§ Β·β π΄) β βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄)))) |
31 | 30 | exp43 438 |
. . . . . . 7
β’ (π§ β β β (π΄ β β β (π΅ β β β (π΅ β 0 β (π₯ = (π§ Β·β π΄) β βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄))))))) |
32 | 31 | com4l 92 |
. . . . . 6
β’ (π΄ β β β (π΅ β β β (π΅ β 0 β (π§ β β β (π₯ = (π§ Β·β π΄) β βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄))))))) |
33 | 32 | 3imp 1112 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π§ β β β (π₯ = (π§ Β·β π΄) β βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄))))) |
34 | 33 | rexlimdv 3151 |
. . . 4
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (βπ§ β β π₯ = (π§ Β·β π΄) β βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄)))) |
35 | 13, 34 | impbid 211 |
. . 3
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄)) β βπ§ β β π₯ = (π§ Β·β π΄))) |
36 | | hvmulcl 29997 |
. . . . . 6
β’ ((π΅ β β β§ π΄ β β) β (π΅
Β·β π΄) β β) |
37 | 36 | ancoms 460 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β (π΅
Β·β π΄) β β) |
38 | | elspansn 30550 |
. . . . 5
β’ ((π΅
Β·β π΄) β β β (π₯ β (spanβ{(π΅ Β·β π΄)}) β βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄)))) |
39 | 37, 38 | syl 17 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β (π₯ β (spanβ{(π΅
Β·β π΄)}) β βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄)))) |
40 | 39 | 3adant3 1133 |
. . 3
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π₯ β (spanβ{(π΅
Β·β π΄)}) β βπ¦ β β π₯ = (π¦ Β·β (π΅
Β·β π΄)))) |
41 | | elspansn 30550 |
. . . 4
β’ (π΄ β β β (π₯ β (spanβ{π΄}) β βπ§ β β π₯ = (π§ Β·β π΄))) |
42 | 41 | 3ad2ant1 1134 |
. . 3
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π₯ β (spanβ{π΄}) β βπ§ β β π₯ = (π§ Β·β π΄))) |
43 | 35, 40, 42 | 3bitr4d 311 |
. 2
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π₯ β (spanβ{(π΅
Β·β π΄)}) β π₯ β (spanβ{π΄}))) |
44 | 43 | eqrdv 2735 |
1
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β
(spanβ{(π΅
Β·β π΄)}) = (spanβ{π΄})) |