Step | Hyp | Ref
| Expression |
1 | | isnvc 24075 |
. . . . . 6
β’ (π β NrmVec β (π β NrmMod β§ π β LVec)) |
2 | 1 | biancomi 464 |
. . . . 5
β’ (π β NrmVec β (π β LVec β§ π β
NrmMod)) |
3 | 2 | a1i 11 |
. . . 4
β’ (π β βVec β (π β NrmVec β (π β LVec β§ π β
NrmMod))) |
4 | | id 22 |
. . . . . 6
β’ (π β βVec β π β
βVec) |
5 | 4 | cvslvec 24504 |
. . . . 5
β’ (π β βVec β π β LVec) |
6 | 5 | biantrurd 534 |
. . . 4
β’ (π β βVec β (π β NrmMod β (π β LVec β§ π β
NrmMod))) |
7 | 4 | cvsclm 24505 |
. . . . 5
β’ (π β βVec β π β
βMod) |
8 | | isncvsngp.v |
. . . . . . 7
β’ π = (Baseβπ) |
9 | | isncvsngp.n |
. . . . . . 7
β’ π = (normβπ) |
10 | | isncvsngp.s |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
11 | | isncvsngp.f |
. . . . . . 7
β’ πΉ = (Scalarβπ) |
12 | | isncvsngp.k |
. . . . . . 7
β’ πΎ = (BaseβπΉ) |
13 | | eqid 2737 |
. . . . . . 7
β’
(normβπΉ) =
(normβπΉ) |
14 | 8, 9, 10, 11, 12, 13 | isnlm 24055 |
. . . . . 6
β’ (π β NrmMod β ((π β NrmGrp β§ π β LMod β§ πΉ β NrmRing) β§
βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯)))) |
15 | | 3anass 1096 |
. . . . . . . . . . 11
β’ ((π β NrmGrp β§ π β LMod β§ πΉ β NrmRing) β (π β NrmGrp β§ (π β LMod β§ πΉ β
NrmRing))) |
16 | 15 | biancomi 464 |
. . . . . . . . . 10
β’ ((π β NrmGrp β§ π β LMod β§ πΉ β NrmRing) β ((π β LMod β§ πΉ β NrmRing) β§ π β
NrmGrp)) |
17 | 16 | anbi1i 625 |
. . . . . . . . 9
β’ (((π β NrmGrp β§ π β LMod β§ πΉ β NrmRing) β§
βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))) β (((π β LMod β§ πΉ β NrmRing) β§ π β NrmGrp) β§ βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯)))) |
18 | | anass 470 |
. . . . . . . . 9
β’ ((((π β LMod β§ πΉ β NrmRing) β§ π β NrmGrp) β§
βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))) β ((π β LMod β§ πΉ β NrmRing) β§ (π β NrmGrp β§ βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))))) |
19 | 17, 18 | bitri 275 |
. . . . . . . 8
β’ (((π β NrmGrp β§ π β LMod β§ πΉ β NrmRing) β§
βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))) β ((π β LMod β§ πΉ β NrmRing) β§ (π β NrmGrp β§ βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))))) |
20 | 19 | a1i 11 |
. . . . . . 7
β’ (π β βMod β
(((π β NrmGrp β§
π β LMod β§ πΉ β NrmRing) β§
βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))) β ((π β LMod β§ πΉ β NrmRing) β§ (π β NrmGrp β§ βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯)))))) |
21 | | clmlmod 24446 |
. . . . . . . . 9
β’ (π β βMod β π β LMod) |
22 | 11, 12 | clmsca 24444 |
. . . . . . . . . 10
β’ (π β βMod β πΉ = (βfld
βΎs πΎ)) |
23 | | cnnrg 24160 |
. . . . . . . . . . 11
β’
βfld β NrmRing |
24 | 11, 12 | clmsubrg 24445 |
. . . . . . . . . . 11
β’ (π β βMod β πΎ β
(SubRingββfld)) |
25 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(βfld βΎs πΎ) = (βfld
βΎs πΎ) |
26 | 25 | subrgnrg 24053 |
. . . . . . . . . . 11
β’
((βfld β NrmRing β§ πΎ β
(SubRingββfld)) β (βfld
βΎs πΎ)
β NrmRing) |
27 | 23, 24, 26 | sylancr 588 |
. . . . . . . . . 10
β’ (π β βMod β
(βfld βΎs πΎ) β NrmRing) |
28 | 22, 27 | eqeltrd 2838 |
. . . . . . . . 9
β’ (π β βMod β πΉ β
NrmRing) |
29 | 21, 28 | jca 513 |
. . . . . . . 8
β’ (π β βMod β (π β LMod β§ πΉ β
NrmRing)) |
30 | 29 | biantrurd 534 |
. . . . . . 7
β’ (π β βMod β
((π β NrmGrp β§
βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))) β ((π β LMod β§ πΉ β NrmRing) β§ (π β NrmGrp β§ βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯)))))) |
31 | | ralcom 3275 |
. . . . . . . . 9
β’
(βπ β
πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯)) β βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))) |
32 | 22 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π β βMod β
(normβπΉ) =
(normβ(βfld βΎs πΎ))) |
33 | | subrgsubg 20244 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ β
(SubRingββfld) β πΎ β
(SubGrpββfld)) |
34 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(normββfld) =
(normββfld) |
35 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(normβ(βfld βΎs πΎ)) = (normβ(βfld
βΎs πΎ)) |
36 | 25, 34, 35 | subgnm 24005 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ β
(SubGrpββfld) β (normβ(βfld
βΎs πΎ)) =
((normββfld) βΎ πΎ)) |
37 | 24, 33, 36 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β βMod β
(normβ(βfld βΎs πΎ)) = ((normββfld)
βΎ πΎ)) |
38 | 32, 37 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (π β βMod β
(normβπΉ) =
((normββfld) βΎ πΎ)) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β βMod β§ (π₯ β π β§ π β πΎ)) β (normβπΉ) = ((normββfld)
βΎ πΎ)) |
40 | 39 | fveq1d 6849 |
. . . . . . . . . . . . 13
β’ ((π β βMod β§ (π₯ β π β§ π β πΎ)) β ((normβπΉ)βπ) = (((normββfld)
βΎ πΎ)βπ)) |
41 | | cnfldnm 24158 |
. . . . . . . . . . . . . . . . 17
β’ abs =
(normββfld) |
42 | 41 | eqcomi 2746 |
. . . . . . . . . . . . . . . 16
β’
(normββfld) = abs |
43 | 42 | reseq1i 5938 |
. . . . . . . . . . . . . . 15
β’
((normββfld) βΎ πΎ) = (abs βΎ πΎ) |
44 | 43 | fveq1i 6848 |
. . . . . . . . . . . . . 14
β’
(((normββfld) βΎ πΎ)βπ) = ((abs βΎ πΎ)βπ) |
45 | | fvres 6866 |
. . . . . . . . . . . . . . 15
β’ (π β πΎ β ((abs βΎ πΎ)βπ) = (absβπ)) |
46 | 45 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ ((π β βMod β§ (π₯ β π β§ π β πΎ)) β ((abs βΎ πΎ)βπ) = (absβπ)) |
47 | 44, 46 | eqtrid 2789 |
. . . . . . . . . . . . 13
β’ ((π β βMod β§ (π₯ β π β§ π β πΎ)) β
(((normββfld) βΎ πΎ)βπ) = (absβπ)) |
48 | 40, 47 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β βMod β§ (π₯ β π β§ π β πΎ)) β ((normβπΉ)βπ) = (absβπ)) |
49 | 48 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π β βMod β§ (π₯ β π β§ π β πΎ)) β (((normβπΉ)βπ) Β· (πβπ₯)) = ((absβπ) Β· (πβπ₯))) |
50 | 49 | eqeq2d 2748 |
. . . . . . . . . 10
β’ ((π β βMod β§ (π₯ β π β§ π β πΎ)) β ((πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯)) β (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
51 | 50 | 2ralbidva 3211 |
. . . . . . . . 9
β’ (π β βMod β
(βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯)) β βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
52 | 31, 51 | bitrid 283 |
. . . . . . . 8
β’ (π β βMod β
(βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯)) β βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |
53 | 52 | anbi2d 630 |
. . . . . . 7
β’ (π β βMod β
((π β NrmGrp β§
βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))) β (π β NrmGrp β§ βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
54 | 20, 30, 53 | 3bitr2d 307 |
. . . . . 6
β’ (π β βMod β
(((π β NrmGrp β§
π β LMod β§ πΉ β NrmRing) β§
βπ β πΎ βπ₯ β π (πβ(π Β· π₯)) = (((normβπΉ)βπ) Β· (πβπ₯))) β (π β NrmGrp β§ βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
55 | 14, 54 | bitrid 283 |
. . . . 5
β’ (π β βMod β (π β NrmMod β (π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
56 | 7, 55 | syl 17 |
. . . 4
β’ (π β βVec β (π β NrmMod β (π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
57 | 3, 6, 56 | 3bitr2d 307 |
. . 3
β’ (π β βVec β (π β NrmVec β (π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
58 | 57 | pm5.32i 576 |
. 2
β’ ((π β βVec β§ π β NrmVec) β (π β βVec β§ (π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
59 | | elin 3931 |
. . 3
β’ (π β (NrmVec β©
βVec) β (π
β NrmVec β§ π
β βVec)) |
60 | 59 | biancomi 464 |
. 2
β’ (π β (NrmVec β©
βVec) β (π
β βVec β§ π
β NrmVec)) |
61 | | 3anass 1096 |
. 2
β’ ((π β βVec β§ π β NrmGrp β§
βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))) β (π β βVec β§ (π β NrmGrp β§ βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯))))) |
62 | 58, 60, 61 | 3bitr4i 303 |
1
β’ (π β (NrmVec β©
βVec) β (π
β βVec β§ π
β NrmGrp β§ βπ₯ β π βπ β πΎ (πβ(π Β· π₯)) = ((absβπ) Β· (πβπ₯)))) |