Metamath Proof Explorer

Definition df-nlm

Description: A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion df-nlm NrmMod = { 𝑤 ∈ ( NrmGrp ∩ LMod ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ NrmRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnlm ⊢ NrmMod
1 vw ⊢ 𝑤
2 cngp ⊢ NrmGrp
3 clmod ⊢ LMod
4 2 3 cin ⊢ ( NrmGrp ∩ LMod )
5 csca ⊢ Scalar
6 1 cv ⊢ 𝑤
7 6 5 cfv ⊢ ( Scalar ‘ 𝑤 )
8 vf ⊢ 𝑓
9 8 cv ⊢ 𝑓
10 cnrg ⊢ NrmRing
11 9 10 wcel ⊢ 𝑓 ∈ NrmRing
12 vx ⊢ 𝑥
13 cbs ⊢ Base
14 9 13 cfv ⊢ ( Base ‘ 𝑓 )
15 vy ⊢ 𝑦
16 6 13 cfv ⊢ ( Base ‘ 𝑤 )
17 cnm ⊢ norm
18 6 17 cfv ⊢ ( norm ‘ 𝑤 )
19 12 cv ⊢ 𝑥
20 cvsca ⊢ ·𝑠
21 6 20 cfv ⊢ ( ·𝑠 ‘ 𝑤 )
22 15 cv ⊢ 𝑦
23 19 22 21 co ⊢ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 )
24 23 18 cfv ⊢ ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) )
25 9 17 cfv ⊢ ( norm ‘ 𝑓 )
26 19 25 cfv ⊢ ( ( norm ‘ 𝑓 ) ‘ 𝑥 )
27 cmul ⊢ ·
28 22 18 cfv ⊢ ( ( norm ‘ 𝑤 ) ‘ 𝑦 )
29 26 28 27 co ⊢ ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) )
30 24 29 wceq ⊢ ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) )
31 30 15 16 wral ⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) )
32 31 12 14 wral ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) )
33 11 32 wa ⊢ ( 𝑓 ∈ NrmRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) )
34 33 8 7 wsbc ⊢ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ NrmRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) )
35 34 1 4 crab ⊢ { 𝑤 ∈ ( NrmGrp ∩ LMod ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ NrmRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) ) }
36 0 35 wceq ⊢ NrmMod = { 𝑤 ∈ ( NrmGrp ∩ LMod ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ NrmRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑓 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( norm ‘ 𝑤 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( ( ( norm ‘ 𝑓 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑤 ) ‘ 𝑦 ) ) ) }