Step | Hyp | Ref
| Expression |
1 | | nlmngp 24064 |
. . . 4
β’ (π β NrmMod β π β NrmGrp) |
2 | | nlmlmod 24065 |
. . . . 5
β’ (π β NrmMod β π β LMod) |
3 | | lssnlm.s |
. . . . . 6
β’ π = (LSubSpβπ) |
4 | 3 | lsssubg 20462 |
. . . . 5
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
5 | 2, 4 | sylan 581 |
. . . 4
β’ ((π β NrmMod β§ π β π) β π β (SubGrpβπ)) |
6 | | lssnlm.x |
. . . . 5
β’ π = (π βΎs π) |
7 | 6 | subgngp 24014 |
. . . 4
β’ ((π β NrmGrp β§ π β (SubGrpβπ)) β π β NrmGrp) |
8 | 1, 5, 7 | syl2an2r 684 |
. . 3
β’ ((π β NrmMod β§ π β π) β π β NrmGrp) |
9 | 6, 3 | lsslmod 20465 |
. . . 4
β’ ((π β LMod β§ π β π) β π β LMod) |
10 | 2, 9 | sylan 581 |
. . 3
β’ ((π β NrmMod β§ π β π) β π β LMod) |
11 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
12 | 6, 11 | resssca 17232 |
. . . . 5
β’ (π β π β (Scalarβπ) = (Scalarβπ)) |
13 | 12 | adantl 483 |
. . . 4
β’ ((π β NrmMod β§ π β π) β (Scalarβπ) = (Scalarβπ)) |
14 | 11 | nlmnrg 24066 |
. . . . 5
β’ (π β NrmMod β
(Scalarβπ) β
NrmRing) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π β NrmMod β§ π β π) β (Scalarβπ) β NrmRing) |
16 | 13, 15 | eqeltrrd 2835 |
. . 3
β’ ((π β NrmMod β§ π β π) β (Scalarβπ) β NrmRing) |
17 | 8, 10, 16 | 3jca 1129 |
. 2
β’ ((π β NrmMod β§ π β π) β (π β NrmGrp β§ π β LMod β§ (Scalarβπ) β
NrmRing)) |
18 | | simpll 766 |
. . . . 5
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β NrmMod) |
19 | | simprl 770 |
. . . . . 6
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π₯ β (Baseβ(Scalarβπ))) |
20 | 13 | adantr 482 |
. . . . . . 7
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (Scalarβπ) = (Scalarβπ)) |
21 | 20 | fveq2d 6850 |
. . . . . 6
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
22 | 19, 21 | eleqtrrd 2837 |
. . . . 5
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π₯ β (Baseβ(Scalarβπ))) |
23 | 5 | adantr 482 |
. . . . . . 7
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β (SubGrpβπ)) |
24 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
25 | 24 | subgss 18937 |
. . . . . . 7
β’ (π β (SubGrpβπ) β π β (Baseβπ)) |
26 | 23, 25 | syl 17 |
. . . . . 6
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β (Baseβπ)) |
27 | | simprr 772 |
. . . . . . 7
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π¦ β (Baseβπ)) |
28 | 6 | subgbas 18940 |
. . . . . . . 8
β’ (π β (SubGrpβπ) β π = (Baseβπ)) |
29 | 23, 28 | syl 17 |
. . . . . . 7
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π = (Baseβπ)) |
30 | 27, 29 | eleqtrrd 2837 |
. . . . . 6
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π¦ β π) |
31 | 26, 30 | sseldd 3949 |
. . . . 5
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π¦ β (Baseβπ)) |
32 | | eqid 2733 |
. . . . . 6
β’
(normβπ) =
(normβπ) |
33 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
34 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
35 | | eqid 2733 |
. . . . . 6
β’
(normβ(Scalarβπ)) = (normβ(Scalarβπ)) |
36 | 24, 32, 33, 11, 34, 35 | nmvs 24063 |
. . . . 5
β’ ((π β NrmMod β§ π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β ((normβπ)β(π₯( Β·π
βπ)π¦)) = (((normβ(Scalarβπ))βπ₯) Β· ((normβπ)βπ¦))) |
37 | 18, 22, 31, 36 | syl3anc 1372 |
. . . 4
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((normβπ)β(π₯( Β·π
βπ)π¦)) = (((normβ(Scalarβπ))βπ₯) Β· ((normβπ)βπ¦))) |
38 | | simplr 768 |
. . . . . . . 8
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β π) |
39 | 6, 33 | ressvsca 17233 |
. . . . . . . 8
β’ (π β π β (
Β·π βπ) = ( Β·π
βπ)) |
40 | 38, 39 | syl 17 |
. . . . . . 7
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (
Β·π βπ) = ( Β·π
βπ)) |
41 | 40 | oveqd 7378 |
. . . . . 6
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)π¦) = (π₯( Β·π
βπ)π¦)) |
42 | 41 | fveq2d 6850 |
. . . . 5
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((normβπ)β(π₯( Β·π
βπ)π¦)) = ((normβπ)β(π₯( Β·π
βπ)π¦))) |
43 | 2 | ad2antrr 725 |
. . . . . . 7
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β LMod) |
44 | 11, 33, 34, 3 | lssvscl 20460 |
. . . . . . 7
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (π₯( Β·π
βπ)π¦) β π) |
45 | 43, 38, 22, 30, 44 | syl22anc 838 |
. . . . . 6
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)π¦) β π) |
46 | | eqid 2733 |
. . . . . . 7
β’
(normβπ) =
(normβπ) |
47 | 6, 32, 46 | subgnm2 24013 |
. . . . . 6
β’ ((π β (SubGrpβπ) β§ (π₯( Β·π
βπ)π¦) β π) β ((normβπ)β(π₯( Β·π
βπ)π¦)) = ((normβπ)β(π₯( Β·π
βπ)π¦))) |
48 | 5, 45, 47 | syl2an2r 684 |
. . . . 5
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((normβπ)β(π₯( Β·π
βπ)π¦)) = ((normβπ)β(π₯( Β·π
βπ)π¦))) |
49 | 42, 48 | eqtr3d 2775 |
. . . 4
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((normβπ)β(π₯( Β·π
βπ)π¦)) = ((normβπ)β(π₯( Β·π
βπ)π¦))) |
50 | 20 | eqcomd 2739 |
. . . . . . 7
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (Scalarβπ) = (Scalarβπ)) |
51 | 50 | fveq2d 6850 |
. . . . . 6
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (normβ(Scalarβπ)) =
(normβ(Scalarβπ))) |
52 | 51 | fveq1d 6848 |
. . . . 5
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((normβ(Scalarβπ))βπ₯) = ((normβ(Scalarβπ))βπ₯)) |
53 | 6, 32, 46 | subgnm2 24013 |
. . . . . 6
β’ ((π β (SubGrpβπ) β§ π¦ β π) β ((normβπ)βπ¦) = ((normβπ)βπ¦)) |
54 | 5, 30, 53 | syl2an2r 684 |
. . . . 5
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((normβπ)βπ¦) = ((normβπ)βπ¦)) |
55 | 52, 54 | oveq12d 7379 |
. . . 4
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (((normβ(Scalarβπ))βπ₯) Β· ((normβπ)βπ¦)) = (((normβ(Scalarβπ))βπ₯) Β· ((normβπ)βπ¦))) |
56 | 37, 49, 55 | 3eqtr4d 2783 |
. . 3
β’ (((π β NrmMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((normβπ)β(π₯( Β·π
βπ)π¦)) = (((normβ(Scalarβπ))βπ₯) Β· ((normβπ)βπ¦))) |
57 | 56 | ralrimivva 3194 |
. 2
β’ ((π β NrmMod β§ π β π) β βπ₯ β (Baseβ(Scalarβπ))βπ¦ β (Baseβπ)((normβπ)β(π₯( Β·π
βπ)π¦)) = (((normβ(Scalarβπ))βπ₯) Β· ((normβπ)βπ¦))) |
58 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
59 | | eqid 2733 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
60 | | eqid 2733 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
61 | | eqid 2733 |
. . 3
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
62 | | eqid 2733 |
. . 3
β’
(normβ(Scalarβπ)) = (normβ(Scalarβπ)) |
63 | 58, 46, 59, 60, 61, 62 | isnlm 24062 |
. 2
β’ (π β NrmMod β ((π β NrmGrp β§ π β LMod β§
(Scalarβπ) β
NrmRing) β§ βπ₯
β (Baseβ(Scalarβπ))βπ¦ β (Baseβπ)((normβπ)β(π₯( Β·π
βπ)π¦)) = (((normβ(Scalarβπ))βπ₯) Β· ((normβπ)βπ¦)))) |
64 | 17, 57, 63 | sylanbrc 584 |
1
β’ ((π β NrmMod β§ π β π) β π β NrmMod) |