Step | Hyp | Ref
| Expression |
1 | | iunss 5006 |
. . . . . . 7
β’ (βͺ π₯ β π΄ π΅ β π β βπ₯ β π΄ π΅ β π) |
2 | | eliun 4959 |
. . . . . . . . . . 11
β’ (π¦ β βͺ π₯ β π΄ π΅ β βπ₯ β π΄ π¦ β π΅) |
3 | 2 | imbi1i 350 |
. . . . . . . . . 10
β’ ((π¦ β βͺ π₯ β π΄ π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β (βπ₯ β π΄ π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
4 | | r19.23v 3176 |
. . . . . . . . . 10
β’
(βπ₯ β
π΄ (π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β (βπ₯ β π΄ π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
5 | 3, 4 | bitr4i 278 |
. . . . . . . . 9
β’ ((π¦ β βͺ π₯ β π΄ π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β βπ₯ β π΄ (π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
6 | 5 | albii 1822 |
. . . . . . . 8
β’
(βπ¦(π¦ β βͺ π₯ β π΄ π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β βπ¦βπ₯ β π΄ (π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
7 | | df-ral 3062 |
. . . . . . . 8
β’
(βπ¦ β
βͺ π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β βπ¦(π¦ β βͺ
π₯ β π΄ π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
8 | | df-ral 3062 |
. . . . . . . . . 10
β’
(βπ¦ β
π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β βπ¦(π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
9 | 8 | ralbii 3093 |
. . . . . . . . 9
β’
(βπ₯ β
π΄ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β βπ₯ β π΄ βπ¦(π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
10 | | ralcom4 3268 |
. . . . . . . . 9
β’
(βπ₯ β
π΄ βπ¦(π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β βπ¦βπ₯ β π΄ (π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
11 | 9, 10 | bitri 275 |
. . . . . . . 8
β’
(βπ₯ β
π΄ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β βπ¦βπ₯ β π΄ (π¦ β π΅ β (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
12 | 6, 7, 11 | 3bitr4i 303 |
. . . . . . 7
β’
(βπ¦ β
βͺ π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β βπ₯ β π΄ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) |
13 | 1, 12 | anbi12i 628 |
. . . . . 6
β’
((βͺ π₯ β π΄ π΅ β π β§ βπ¦ β βͺ
π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β (βπ₯ β π΄ π΅ β π β§ βπ₯ β π΄ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
14 | | r19.26 3111 |
. . . . . 6
β’
(βπ₯ β
π΄ (π΅ β π β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β (βπ₯ β π΄ π΅ β π β§ βπ₯ β π΄ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
15 | 13, 14 | bitr4i 278 |
. . . . 5
β’
((βͺ π₯ β π΄ π΅ β π β§ βπ¦ β βͺ
π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β βπ₯ β π΄ (π΅ β π β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
16 | | eliin 4960 |
. . . . . 6
β’ (π§ β π β (π§ β β©
π₯ β π΄ ( β₯ βπ΅) β βπ₯ β π΄ π§ β ( β₯ βπ΅))) |
17 | | iunocv.v |
. . . . . . . . . 10
β’ π = (Baseβπ) |
18 | | eqid 2733 |
. . . . . . . . . 10
β’
(Β·πβπ) =
(Β·πβπ) |
19 | | eqid 2733 |
. . . . . . . . . 10
β’
(Scalarβπ) =
(Scalarβπ) |
20 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
21 | | inocv.o |
. . . . . . . . . 10
β’ β₯ =
(ocvβπ) |
22 | 17, 18, 19, 20, 21 | elocv 21088 |
. . . . . . . . 9
β’ (π§ β ( β₯ βπ΅) β (π΅ β π β§ π§ β π β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
23 | | 3anan12 1097 |
. . . . . . . . 9
β’ ((π΅ β π β§ π§ β π β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β (π§ β π β§ (π΅ β π β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
24 | 22, 23 | bitri 275 |
. . . . . . . 8
β’ (π§ β ( β₯ βπ΅) β (π§ β π β§ (π΅ β π β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
25 | 24 | baib 537 |
. . . . . . 7
β’ (π§ β π β (π§ β ( β₯ βπ΅) β (π΅ β π β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
26 | 25 | ralbidv 3171 |
. . . . . 6
β’ (π§ β π β (βπ₯ β π΄ π§ β ( β₯ βπ΅) β βπ₯ β π΄ (π΅ β π β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
27 | 16, 26 | bitr2d 280 |
. . . . 5
β’ (π§ β π β (βπ₯ β π΄ (π΅ β π β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β π§ β β©
π₯ β π΄ ( β₯ βπ΅))) |
28 | 15, 27 | bitrid 283 |
. . . 4
β’ (π§ β π β ((βͺ π₯ β π΄ π΅ β π β§ βπ¦ β βͺ
π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β π§ β β©
π₯ β π΄ ( β₯ βπ΅))) |
29 | 28 | pm5.32i 576 |
. . 3
β’ ((π§ β π β§ (βͺ
π₯ β π΄ π΅ β π β§ βπ¦ β βͺ
π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) β (π§ β π β§ π§ β β©
π₯ β π΄ ( β₯ βπ΅))) |
30 | 17, 18, 19, 20, 21 | elocv 21088 |
. . . 4
β’ (π§ β ( β₯ ββͺ π₯ β π΄ π΅) β (βͺ π₯ β π΄ π΅ β π β§ π§ β π β§ βπ¦ β βͺ
π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
31 | | 3anan12 1097 |
. . . 4
β’
((βͺ π₯ β π΄ π΅ β π β§ π§ β π β§ βπ¦ β βͺ
π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β (π§ β π β§ (βͺ
π₯ β π΄ π΅ β π β§ βπ¦ β βͺ
π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
32 | 30, 31 | bitri 275 |
. . 3
β’ (π§ β ( β₯ ββͺ π₯ β π΄ π΅) β (π§ β π β§ (βͺ
π₯ β π΄ π΅ β π β§ βπ¦ β βͺ
π₯ β π΄ π΅(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
33 | | elin 3927 |
. . 3
β’ (π§ β (π β© β©
π₯ β π΄ ( β₯ βπ΅)) β (π§ β π β§ π§ β β©
π₯ β π΄ ( β₯ βπ΅))) |
34 | 29, 32, 33 | 3bitr4i 303 |
. 2
β’ (π§ β ( β₯ ββͺ π₯ β π΄ π΅) β π§ β (π β© β©
π₯ β π΄ ( β₯ βπ΅))) |
35 | 34 | eqriv 2730 |
1
β’ ( β₯
ββͺ π₯ β π΄ π΅) = (π β© β©
π₯ β π΄ ( β₯ βπ΅)) |