Step | Hyp | Ref
| Expression |
1 | | eqidd 2737 |
. 2
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β (Scalarβπ) = (Scalarβπ)) |
2 | | eqidd 2737 |
. 2
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ))) |
3 | | eqidd 2737 |
. 2
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β (Baseβπ) = (Baseβπ)) |
4 | | eqidd 2737 |
. 2
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β
(+gβπ) =
(+gβπ)) |
5 | | eqidd 2737 |
. 2
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β (
Β·π βπ) = ( Β·π
βπ)) |
6 | | lssintcl.s |
. . 3
β’ π = (LSubSpβπ) |
7 | 6 | a1i 11 |
. 2
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β π = (LSubSpβπ)) |
8 | | intssuni2 4932 |
. . . 4
β’ ((π΄ β π β§ π΄ β β
) β β© π΄
β βͺ π) |
9 | 8 | 3adant1 1130 |
. . 3
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β β© π΄
β βͺ π) |
10 | | eqid 2736 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
11 | 10, 6 | lssss 20382 |
. . . . . 6
β’ (π¦ β π β π¦ β (Baseβπ)) |
12 | | velpw 4563 |
. . . . . 6
β’ (π¦ β π«
(Baseβπ) β π¦ β (Baseβπ)) |
13 | 11, 12 | sylibr 233 |
. . . . 5
β’ (π¦ β π β π¦ β π« (Baseβπ)) |
14 | 13 | ssriv 3946 |
. . . 4
β’ π β π«
(Baseβπ) |
15 | | sspwuni 5058 |
. . . 4
β’ (π β π«
(Baseβπ) β βͺ π
β (Baseβπ)) |
16 | 14, 15 | mpbi 229 |
. . 3
β’ βͺ π
β (Baseβπ) |
17 | 9, 16 | sstrdi 3954 |
. 2
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β β© π΄
β (Baseβπ)) |
18 | | simpl1 1191 |
. . . . . 6
β’ (((π β LMod β§ π΄ β π β§ π΄ β β
) β§ π¦ β π΄) β π β LMod) |
19 | | simp2 1137 |
. . . . . . 7
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β π΄ β π) |
20 | 19 | sselda 3942 |
. . . . . 6
β’ (((π β LMod β§ π΄ β π β§ π΄ β β
) β§ π¦ β π΄) β π¦ β π) |
21 | | eqid 2736 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
22 | 21, 6 | lss0cl 20392 |
. . . . . 6
β’ ((π β LMod β§ π¦ β π) β (0gβπ) β π¦) |
23 | 18, 20, 22 | syl2anc 584 |
. . . . 5
β’ (((π β LMod β§ π΄ β π β§ π΄ β β
) β§ π¦ β π΄) β (0gβπ) β π¦) |
24 | 23 | ralrimiva 3141 |
. . . 4
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β βπ¦ β π΄ (0gβπ) β π¦) |
25 | | fvex 6852 |
. . . . 5
β’
(0gβπ) β V |
26 | 25 | elint2 4912 |
. . . 4
β’
((0gβπ) β β© π΄ β βπ¦ β π΄ (0gβπ) β π¦) |
27 | 24, 26 | sylibr 233 |
. . 3
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β
(0gβπ)
β β© π΄) |
28 | 27 | ne0d 4293 |
. 2
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β β© π΄
β β
) |
29 | 20 | adantlr 713 |
. . . . 5
β’ ((((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β§ π¦ β π΄) β π¦ β π) |
30 | | simplr1 1215 |
. . . . 5
β’ ((((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β§ π¦ β π΄) β π₯ β (Baseβ(Scalarβπ))) |
31 | | simplr2 1216 |
. . . . . 6
β’ ((((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β§ π¦ β π΄) β π β β© π΄) |
32 | | simpr 485 |
. . . . . 6
β’ ((((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β§ π¦ β π΄) β π¦ β π΄) |
33 | | elinti 4914 |
. . . . . 6
β’ (π β β© π΄
β (π¦ β π΄ β π β π¦)) |
34 | 31, 32, 33 | sylc 65 |
. . . . 5
β’ ((((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β§ π¦ β π΄) β π β π¦) |
35 | | simplr3 1217 |
. . . . . 6
β’ ((((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β§ π¦ β π΄) β π β β© π΄) |
36 | | elinti 4914 |
. . . . . 6
β’ (π β β© π΄
β (π¦ β π΄ β π β π¦)) |
37 | 35, 32, 36 | sylc 65 |
. . . . 5
β’ ((((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β§ π¦ β π΄) β π β π¦) |
38 | | eqid 2736 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
39 | | eqid 2736 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
40 | | eqid 2736 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
41 | | eqid 2736 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
42 | 38, 39, 40, 41, 6 | lsscl 20388 |
. . . . 5
β’ ((π¦ β π β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π¦ β§ π β π¦)) β ((π₯( Β·π
βπ)π)(+gβπ)π) β π¦) |
43 | 29, 30, 34, 37, 42 | syl13anc 1372 |
. . . 4
β’ ((((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β§ π¦ β π΄) β ((π₯( Β·π
βπ)π)(+gβπ)π) β π¦) |
44 | 43 | ralrimiva 3141 |
. . 3
β’ (((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β βπ¦ β π΄ ((π₯( Β·π
βπ)π)(+gβπ)π) β π¦) |
45 | | ovex 7386 |
. . . 4
β’ ((π₯(
Β·π βπ)π)(+gβπ)π) β V |
46 | 45 | elint2 4912 |
. . 3
β’ (((π₯(
Β·π βπ)π)(+gβπ)π) β β© π΄ β βπ¦ β π΄ ((π₯( Β·π
βπ)π)(+gβπ)π) β π¦) |
47 | 44, 46 | sylibr 233 |
. 2
β’ (((π β LMod β§ π΄ β π β§ π΄ β β
) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β β© π΄ β§ π β β© π΄)) β ((π₯( Β·π
βπ)π)(+gβπ)π) β β© π΄) |
48 | 1, 2, 3, 4, 5, 7, 17, 28, 47 | islssd 20381 |
1
β’ ((π β LMod β§ π΄ β π β§ π΄ β β
) β β© π΄
β π) |