Step | Hyp | Ref
| Expression |
1 | | issubassa2.a |
. . . . 5
β’ π΄ = (algScβπ) |
2 | | eqid 2733 |
. . . . 5
β’
(1rβπ) = (1rβπ) |
3 | | eqid 2733 |
. . . . 5
β’
(LSpanβπ) =
(LSpanβπ) |
4 | 1, 2, 3 | rnascl 21310 |
. . . 4
β’ (π β AssAlg β ran π΄ = ((LSpanβπ)β{(1rβπ)})) |
5 | 4 | ad2antrr 725 |
. . 3
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ π β πΏ) β ran π΄ = ((LSpanβπ)β{(1rβπ)})) |
6 | | issubassa2.l |
. . . 4
β’ πΏ = (LSubSpβπ) |
7 | | assalmod 21282 |
. . . . 5
β’ (π β AssAlg β π β LMod) |
8 | 7 | ad2antrr 725 |
. . . 4
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ π β πΏ) β π β LMod) |
9 | | simpr 486 |
. . . 4
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ π β πΏ) β π β πΏ) |
10 | 2 | subrg1cl 20244 |
. . . . 5
β’ (π β (SubRingβπ) β
(1rβπ)
β π) |
11 | 10 | ad2antlr 726 |
. . . 4
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ π β πΏ) β (1rβπ) β π) |
12 | 6, 3, 8, 9, 11 | lspsnel5a 20472 |
. . 3
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ π β πΏ) β ((LSpanβπ)β{(1rβπ)}) β π) |
13 | 5, 12 | eqsstrd 3983 |
. 2
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ π β πΏ) β ran π΄ β π) |
14 | | subrgsubg 20242 |
. . . 4
β’ (π β (SubRingβπ) β π β (SubGrpβπ)) |
15 | 14 | ad2antlr 726 |
. . 3
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β π β (SubGrpβπ)) |
16 | | simplll 774 |
. . . . . 6
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π β AssAlg) |
17 | | simprl 770 |
. . . . . 6
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π₯ β (Baseβ(Scalarβπ))) |
18 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
19 | 18 | subrgss 20237 |
. . . . . . . . 9
β’ (π β (SubRingβπ) β π β (Baseβπ)) |
20 | 19 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β π β (Baseβπ)) |
21 | 20 | sselda 3945 |
. . . . . . 7
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ π¦ β π) β π¦ β (Baseβπ)) |
22 | 21 | adantrl 715 |
. . . . . 6
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π¦ β (Baseβπ)) |
23 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
24 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
25 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ) = (.rβπ) |
26 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
27 | 1, 23, 24, 18, 25, 26 | asclmul1 21305 |
. . . . . 6
β’ ((π β AssAlg β§ π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β ((π΄βπ₯)(.rβπ)π¦) = (π₯( Β·π
βπ)π¦)) |
28 | 16, 17, 22, 27 | syl3anc 1372 |
. . . . 5
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β ((π΄βπ₯)(.rβπ)π¦) = (π₯( Β·π
βπ)π¦)) |
29 | | simpllr 775 |
. . . . . 6
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π β (SubRingβπ)) |
30 | | simplr 768 |
. . . . . . . 8
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ π₯ β (Baseβ(Scalarβπ))) β ran π΄ β π) |
31 | 1, 23, 24 | asclfn 21300 |
. . . . . . . . . 10
β’ π΄ Fn
(Baseβ(Scalarβπ)) |
32 | 31 | a1i 11 |
. . . . . . . . 9
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β π΄ Fn (Baseβ(Scalarβπ))) |
33 | | fnfvelrn 7032 |
. . . . . . . . 9
β’ ((π΄ Fn
(Baseβ(Scalarβπ)) β§ π₯ β (Baseβ(Scalarβπ))) β (π΄βπ₯) β ran π΄) |
34 | 32, 33 | sylan 581 |
. . . . . . . 8
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ π₯ β (Baseβ(Scalarβπ))) β (π΄βπ₯) β ran π΄) |
35 | 30, 34 | sseldd 3946 |
. . . . . . 7
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ π₯ β (Baseβ(Scalarβπ))) β (π΄βπ₯) β π) |
36 | 35 | adantrr 716 |
. . . . . 6
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (π΄βπ₯) β π) |
37 | | simprr 772 |
. . . . . 6
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π¦ β π) |
38 | 25 | subrgmcl 20248 |
. . . . . 6
β’ ((π β (SubRingβπ) β§ (π΄βπ₯) β π β§ π¦ β π) β ((π΄βπ₯)(.rβπ)π¦) β π) |
39 | 29, 36, 37, 38 | syl3anc 1372 |
. . . . 5
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β ((π΄βπ₯)(.rβπ)π¦) β π) |
40 | 28, 39 | eqeltrrd 2835 |
. . . 4
β’ ((((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (π₯( Β·π
βπ)π¦) β π) |
41 | 40 | ralrimivva 3194 |
. . 3
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π) |
42 | 23, 24, 18, 26, 6 | islss4 20438 |
. . . . 5
β’ (π β LMod β (π β πΏ β (π β (SubGrpβπ) β§ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π))) |
43 | 7, 42 | syl 17 |
. . . 4
β’ (π β AssAlg β (π β πΏ β (π β (SubGrpβπ) β§ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π))) |
44 | 43 | ad2antrr 725 |
. . 3
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β (π β πΏ β (π β (SubGrpβπ) β§ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π))) |
45 | 15, 41, 44 | mpbir2and 712 |
. 2
β’ (((π β AssAlg β§ π β (SubRingβπ)) β§ ran π΄ β π) β π β πΏ) |
46 | 13, 45 | impbida 800 |
1
β’ ((π β AssAlg β§ π β (SubRingβπ)) β (π β πΏ β ran π΄ β π)) |