Step | Hyp | Ref
| Expression |
1 | | anass 679 |
. 2
⊢ (((𝑊 ∈ (NrmGrp ∩ LMod)
∧ 𝐹 ∈ NrmRing)
∧ ∀𝑥 ∈
𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦))) ↔ (𝑊 ∈ (NrmGrp ∩ LMod) ∧ (𝐹 ∈ NrmRing ∧
∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦))))) |
2 | | df-3an 1033 |
. . . 4
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod) ∧ 𝐹 ∈
NrmRing)) |
3 | | elin 3758 |
. . . . 5
⊢ (𝑊 ∈ (NrmGrp ∩ LMod)
↔ (𝑊 ∈ NrmGrp
∧ 𝑊 ∈
LMod)) |
4 | 3 | anbi1i 727 |
. . . 4
⊢ ((𝑊 ∈ (NrmGrp ∩ LMod)
∧ 𝐹 ∈ NrmRing)
↔ ((𝑊 ∈ NrmGrp
∧ 𝑊 ∈ LMod) ∧
𝐹 ∈
NrmRing)) |
5 | 2, 4 | bitr4i 266 |
. . 3
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ↔ (𝑊 ∈ (NrmGrp ∩ LMod)
∧ 𝐹 ∈
NrmRing)) |
6 | 5 | anbi1i 727 |
. 2
⊢ (((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧
∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦))) ↔ ((𝑊 ∈ (NrmGrp ∩ LMod) ∧ 𝐹 ∈ NrmRing) ∧
∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦)))) |
7 | | fvex 6113 |
. . . . 5
⊢
(Scalar‘𝑤)
∈ V |
8 | 7 | a1i 11 |
. . . 4
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V) |
9 | | id 22 |
. . . . . . 7
⊢ (𝑓 = (Scalar‘𝑤) → 𝑓 = (Scalar‘𝑤)) |
10 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
11 | | isnlm.f |
. . . . . . . 8
⊢ 𝐹 = (Scalar‘𝑊) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹) |
13 | 9, 12 | sylan9eqr 2666 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → 𝑓 = 𝐹) |
14 | 13 | eleq1d 2672 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (𝑓 ∈ NrmRing ↔ 𝐹 ∈ NrmRing)) |
15 | 13 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑓) = (Base‘𝐹)) |
16 | | isnlm.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝐹) |
17 | 15, 16 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑓) = 𝐾) |
18 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → 𝑤 = 𝑊) |
19 | 18 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑤) = (Base‘𝑊)) |
20 | | isnlm.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) |
21 | 19, 20 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑤) = 𝑉) |
22 | 18 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (norm‘𝑤) = (norm‘𝑊)) |
23 | | isnlm.n |
. . . . . . . . . 10
⊢ 𝑁 = (norm‘𝑊) |
24 | 22, 23 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (norm‘𝑤) = 𝑁) |
25 | 18 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (
·𝑠 ‘𝑤) = ( ·𝑠
‘𝑊)) |
26 | | isnlm.s |
. . . . . . . . . . 11
⊢ · = (
·𝑠 ‘𝑊) |
27 | 25, 26 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (
·𝑠 ‘𝑤) = · ) |
28 | 27 | oveqd 6566 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (𝑥( ·𝑠
‘𝑤)𝑦) = (𝑥 · 𝑦)) |
29 | 24, 28 | fveq12d 6109 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → ((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (𝑁‘(𝑥 · 𝑦))) |
30 | 13 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (norm‘𝑓) = (norm‘𝐹)) |
31 | | isnlm.a |
. . . . . . . . . . 11
⊢ 𝐴 = (norm‘𝐹) |
32 | 30, 31 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (norm‘𝑓) = 𝐴) |
33 | 32 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → ((norm‘𝑓)‘𝑥) = (𝐴‘𝑥)) |
34 | 24 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → ((norm‘𝑤)‘𝑦) = (𝑁‘𝑦)) |
35 | 33, 34 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦))) |
36 | 29, 35 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)) ↔ (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦)))) |
37 | 21, 36 | raleqbidv 3129 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)) ↔ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦)))) |
38 | 17, 37 | raleqbidv 3129 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)) ↔ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦)))) |
39 | 14, 38 | anbi12d 743 |
. . . 4
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → ((𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))) ↔ (𝐹 ∈ NrmRing ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦))))) |
40 | 8, 39 | sbcied 3439 |
. . 3
⊢ (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))) ↔ (𝐹 ∈ NrmRing ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦))))) |
41 | | df-nlm 22201 |
. . 3
⊢ NrmMod =
{𝑤 ∈ (NrmGrp ∩
LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))} |
42 | 40, 41 | elrab2 3333 |
. 2
⊢ (𝑊 ∈ NrmMod ↔ (𝑊 ∈ (NrmGrp ∩ LMod)
∧ (𝐹 ∈ NrmRing
∧ ∀𝑥 ∈
𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦))))) |
43 | 1, 6, 42 | 3bitr4ri 292 |
1
⊢ (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧
∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦)))) |