Metamath Proof Explorer

Theorem islmhm

Description: Property of being a homomorphism of left modules. (Contributed by Stefan O'Rear, 1-Jan-2015) (Proof shortened by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses islmhm.k ⊢ 𝐾 = ( Scalar ‘ 𝑆 )
islmhm.l ⊢ 𝐿 = ( Scalar ‘ 𝑇 )
islmhm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
islmhm.e ⊢ 𝐸 = ( Base ‘ 𝑆 )
islmhm.m ⊢ · = ( ·𝑠 ‘ 𝑆 )
islmhm.n ⊢ × = ( ·𝑠 ‘ 𝑇 )
Assertion islmhm ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islmhm.k ⊢ 𝐾 = ( Scalar ‘ 𝑆 )
2 islmhm.l ⊢ 𝐿 = ( Scalar ‘ 𝑇 )
3 islmhm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
4 islmhm.e ⊢ 𝐸 = ( Base ‘ 𝑆 )
5 islmhm.m ⊢ · = ( ·𝑠 ‘ 𝑆 )
6 islmhm.n ⊢ × = ( ·𝑠 ‘ 𝑇 )
7 df-lmhm ⊢ LMHom = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
8 7 elmpocl ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) )
9 oveq12 ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 GrpHom 𝑡 ) = ( 𝑆 GrpHom 𝑇 ) )
10 fvexd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( Scalar ‘ 𝑠 ) ∈ V )
11 simplr ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → 𝑡 = 𝑇 )
12 11 fveq2d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( Scalar ‘ 𝑡 ) = ( Scalar ‘ 𝑇 ) )
13 12 2 eqtr4di ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( Scalar ‘ 𝑡 ) = 𝐿 )
14 simpr ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → 𝑤 = ( Scalar ‘ 𝑠 ) )
15 simpll ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → 𝑠 = 𝑆 )
16 15 fveq2d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( Scalar ‘ 𝑠 ) = ( Scalar ‘ 𝑆 ) )
17 14 16 eqtrd ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → 𝑤 = ( Scalar ‘ 𝑆 ) )
18 17 1 eqtr4di ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → 𝑤 = 𝐾 )
19 13 18 eqeq12d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( ( Scalar ‘ 𝑡 ) = 𝑤 ↔ 𝐿 = 𝐾 ) )
20 18 fveq2d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( Base ‘ 𝑤 ) = ( Base ‘ 𝐾 ) )
21 20 3 eqtr4di ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( Base ‘ 𝑤 ) = 𝐵 )
22 15 fveq2d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
23 22 4 eqtr4di ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( Base ‘ 𝑠 ) = 𝐸 )
24 15 fveq2d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( ·𝑠 ‘ 𝑠 ) = ( ·𝑠 ‘ 𝑆 ) )
25 24 5 eqtr4di ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( ·𝑠 ‘ 𝑠 ) = · )
26 25 oveqd ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
27 26 fveq2d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) )
28 11 fveq2d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( ·𝑠 ‘ 𝑡 ) = ( ·𝑠 ‘ 𝑇 ) )
29 28 6 eqtr4di ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( ·𝑠 ‘ 𝑡 ) = × )
30 29 oveqd ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) )
31 27 30 eqeq12d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) )
32 23 31 raleqbidv ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) )
33 21 32 raleqbidv ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) )
34 19 33 anbi12d ⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) ∧ 𝑤 = ( Scalar ‘ 𝑠 ) ) → ( ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) ) )
35 10 34 sbcied ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) ) )
36 9 35 rabeqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → { 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) } = { 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ∣ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) } )
37 ovex ⊢ ( 𝑆 GrpHom 𝑇 ) ∈ V
38 37 rabex ⊢ { 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ∣ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V
39 36 7 38 ovmpoa ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) → ( 𝑆 LMHom 𝑇 ) = { 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ∣ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) } )
40 39 eleq2d ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) → ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ∣ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) } ) )
41 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) )
42 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
43 42 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) )
44 41 43 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) )
45 44 2ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) )
46 45 anbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )
47 46 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ∣ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )
48 3anass ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )
49 47 48 bitr4i ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ∣ ( 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) )
50 40 49 bitrdi ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) → ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )
51 8 50 biadanii ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )