This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-lmhm

Description: A homomorphism of left modules is a group homomorphism which additionally preserves the scalar product. This requires both structures to be left modules over the same ring. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Assertion df-lmhm LMHom = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmhm ⊢ LMHom
1 vs ⊢ 𝑠
2 clmod ⊢ LMod
3 vt ⊢ 𝑡
4 vf ⊢ 𝑓
5 1 cv ⊢ 𝑠
6 cghm ⊢ GrpHom
7 3 cv ⊢ 𝑡
8 5 7 6 co ⊢ ( 𝑠 GrpHom 𝑡 )
9 csca ⊢ Scalar
10 5 9 cfv ⊢ ( Scalar ‘ 𝑠 )
11 vw ⊢ 𝑤
12 7 9 cfv ⊢ ( Scalar ‘ 𝑡 )
13 11 cv ⊢ 𝑤
14 12 13 wceq ⊢ ( Scalar ‘ 𝑡 ) = 𝑤
15 vx ⊢ 𝑥
16 cbs ⊢ Base
17 13 16 cfv ⊢ ( Base ‘ 𝑤 )
18 vy ⊢ 𝑦
19 5 16 cfv ⊢ ( Base ‘ 𝑠 )
20 4 cv ⊢ 𝑓
21 15 cv ⊢ 𝑥
22 cvsca ⊢ ·𝑠
23 5 22 cfv ⊢ ( ·𝑠 ‘ 𝑠 )
24 18 cv ⊢ 𝑦
25 21 24 23 co ⊢ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 )
26 25 20 cfv ⊢ ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) )
27 7 22 cfv ⊢ ( ·𝑠 ‘ 𝑡 )
28 24 20 cfv ⊢ ( 𝑓 ‘ 𝑦 )
29 21 28 27 co ⊢ ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
30 26 29 wceq ⊢ ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
31 30 18 19 wral ⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
32 31 15 17 wral ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
33 14 32 wa ⊢ ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) )
34 33 11 10 wsbc ⊢ [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) )
35 34 4 8 crab ⊢ { 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) }
36 1 3 2 2 35 cmpo ⊢ ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
37 0 36 wceq ⊢ LMHom = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) } )