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 ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) } )