Step | Hyp | Ref
| Expression |
1 | | unss 4145 |
. . . . . . 7
β’ ((π΄ β (Baseβπ) β§ π΅ β (Baseβπ)) β (π΄ βͺ π΅) β (Baseβπ)) |
2 | 1 | bicomi 223 |
. . . . . 6
β’ ((π΄ βͺ π΅) β (Baseβπ) β (π΄ β (Baseβπ) β§ π΅ β (Baseβπ))) |
3 | | ralunb 4152 |
. . . . . 6
β’
(βπ¦ β
(π΄ βͺ π΅)(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β (βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
4 | 2, 3 | anbi12i 628 |
. . . . 5
β’ (((π΄ βͺ π΅) β (Baseβπ) β§ βπ¦ β (π΄ βͺ π΅)(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β ((π΄ β (Baseβπ) β§ π΅ β (Baseβπ)) β§ (βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
5 | | an4 655 |
. . . . 5
β’ (((π΄ β (Baseβπ) β§ π΅ β (Baseβπ)) β§ (βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) β ((π΄ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β§ (π΅ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
6 | 4, 5 | bitri 275 |
. . . 4
β’ (((π΄ βͺ π΅) β (Baseβπ) β§ βπ¦ β (π΄ βͺ π΅)(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β ((π΄ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β§ (π΅ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
7 | 6 | anbi2i 624 |
. . 3
β’ ((π§ β (Baseβπ) β§ ((π΄ βͺ π΅) β (Baseβπ) β§ βπ¦ β (π΄ βͺ π΅)(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) β (π§ β (Baseβπ) β§ ((π΄ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β§ (π΅ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))))) |
8 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
9 | | eqid 2733 |
. . . . 5
β’
(Β·πβπ) =
(Β·πβπ) |
10 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
11 | | eqid 2733 |
. . . . 5
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
12 | | inocv.o |
. . . . 5
β’ β₯ =
(ocvβπ) |
13 | 8, 9, 10, 11, 12 | elocv 21088 |
. . . 4
β’ (π§ β ( β₯ β(π΄ βͺ π΅)) β ((π΄ βͺ π΅) β (Baseβπ) β§ π§ β (Baseβπ) β§ βπ¦ β (π΄ βͺ π΅)(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
14 | | 3anan12 1097 |
. . . 4
β’ (((π΄ βͺ π΅) β (Baseβπ) β§ π§ β (Baseβπ) β§ βπ¦ β (π΄ βͺ π΅)(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β (π§ β (Baseβπ) β§ ((π΄ βͺ π΅) β (Baseβπ) β§ βπ¦ β (π΄ βͺ π΅)(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
15 | 13, 14 | bitri 275 |
. . 3
β’ (π§ β ( β₯ β(π΄ βͺ π΅)) β (π§ β (Baseβπ) β§ ((π΄ βͺ π΅) β (Baseβπ) β§ βπ¦ β (π΄ βͺ π΅)(π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
16 | 8, 9, 10, 11, 12 | elocv 21088 |
. . . . . 6
β’ (π§ β ( β₯ βπ΄) β (π΄ β (Baseβπ) β§ π§ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
17 | | 3anan12 1097 |
. . . . . 6
β’ ((π΄ β (Baseβπ) β§ π§ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β (π§ β (Baseβπ) β§ (π΄ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
18 | 16, 17 | bitri 275 |
. . . . 5
β’ (π§ β ( β₯ βπ΄) β (π§ β (Baseβπ) β§ (π΄ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
19 | 8, 9, 10, 11, 12 | elocv 21088 |
. . . . . 6
β’ (π§ β ( β₯ βπ΅) β (π΅ β (Baseβπ) β§ π§ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) |
20 | | 3anan12 1097 |
. . . . . 6
β’ ((π΅ β (Baseβπ) β§ π§ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β (π§ β (Baseβπ) β§ (π΅ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
21 | 19, 20 | bitri 275 |
. . . . 5
β’ (π§ β ( β₯ βπ΅) β (π§ β (Baseβπ) β§ (π΅ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) |
22 | 18, 21 | anbi12i 628 |
. . . 4
β’ ((π§ β ( β₯ βπ΄) β§ π§ β ( β₯ βπ΅)) β ((π§ β (Baseβπ) β§ (π΄ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) β§ (π§ β (Baseβπ) β§ (π΅ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))))) |
23 | | elin 3927 |
. . . 4
β’ (π§ β (( β₯ βπ΄) β© ( β₯ βπ΅)) β (π§ β ( β₯ βπ΄) β§ π§ β ( β₯ βπ΅))) |
24 | | anandi 675 |
. . . 4
β’ ((π§ β (Baseβπ) β§ ((π΄ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β§ (π΅ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))))) β ((π§ β (Baseβπ) β§ (π΄ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))) β§ (π§ β (Baseβπ) β§ (π΅ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))))) |
25 | 22, 23, 24 | 3bitr4i 303 |
. . 3
β’ (π§ β (( β₯ βπ΄) β© ( β₯ βπ΅)) β (π§ β (Baseβπ) β§ ((π΄ β (Baseβπ) β§ βπ¦ β π΄ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ))) β§ (π΅ β (Baseβπ) β§ βπ¦ β π΅ (π§(Β·πβπ)π¦) = (0gβ(Scalarβπ)))))) |
26 | 7, 15, 25 | 3bitr4i 303 |
. 2
β’ (π§ β ( β₯ β(π΄ βͺ π΅)) β π§ β (( β₯ βπ΄) β© ( β₯ βπ΅))) |
27 | 26 | eqriv 2730 |
1
β’ ( β₯
β(π΄ βͺ π΅)) = (( β₯ βπ΄) β© ( β₯ βπ΅)) |