Theorem islmhm 19027

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.)

Hypotheses

Ref	Expression
islmhm.k	|- K = (Scalar ` S )
islmhm.l	|- L = (Scalar ` T )
islmhm.b	|- B = ( Base ` K )
islmhm.e	|- E = ( Base ` S )
islmhm.m	|- .x. = ( .s ` S )
islmhm.n	|- .X. = ( .s ` T )

Assertion

Ref	Expression
islmhm	|- ( F e. ( S LMHom T ) <-> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )

Distinct variable groups:   x, B   y, E   x, y, S   x, F, y   x, T, y

Allowed substitution hints:   B( y)   .x. ( x, y)   .X. ( x, y)   E( x)   K( x, y)   L( x, y)

Proof of Theorem islmhm

Dummy variables f s t w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-lmhm 19022	. . 3 |- LMHom = ( s e. LMod , t e. LMod |-> { f e. ( s GrpHom t ) | [. (Scalar ` s ) / w ]. ( (Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) } )
2	1	elmpt2cl 6876	. 2 |- ( F e. ( S LMHom T ) -> ( S e. LMod /\ T e. LMod ) )
3		oveq12 6659	. . . . . 6 |- ( ( s = S /\ t = T ) -> ( s GrpHom t ) = ( S GrpHom T ) )
4		fvexd 6203	. . . . . . 7 |- ( ( s = S /\ t = T ) -> (Scalar ` s ) e. _V )
5		simplr 792	. . . . . . . . . . 11 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> t = T )
6	5	fveq2d 6195	. . . . . . . . . 10 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> (Scalar ` t ) = (Scalar ` T ) )
7		islmhm.l	. . . . . . . . . 10 |- L = (Scalar ` T )
8	6, 7	syl6eqr 2674	. . . . . . . . 9 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> (Scalar ` t ) = L )
9		simpr 477	. . . . . . . . . . 11 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> w = (Scalar ` s ) )
10		simpll 790	. . . . . . . . . . . 12 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> s = S )
11	10	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> (Scalar ` s ) = (Scalar ` S ) )
12	9, 11	eqtrd 2656	. . . . . . . . . 10 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> w = (Scalar ` S ) )
13		islmhm.k	. . . . . . . . . 10 |- K = (Scalar ` S )
14	12, 13	syl6eqr 2674	. . . . . . . . 9 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> w = K )
15	8, 14	eqeq12d 2637	. . . . . . . 8 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( (Scalar ` t ) = w <-> L = K ) )
16	14	fveq2d 6195	. . . . . . . . . 10 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( Base ` w ) = ( Base ` K ) )
17		islmhm.b	. . . . . . . . . 10 |- B = ( Base ` K )
18	16, 17	syl6eqr 2674	. . . . . . . . 9 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( Base ` w ) = B )
19	10	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( Base ` s ) = ( Base ` S ) )
20		islmhm.e	. . . . . . . . . . 11 |- E = ( Base ` S )
21	19, 20	syl6eqr 2674	. . . . . . . . . 10 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( Base ` s ) = E )
22	10	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( .s ` s ) = ( .s ` S ) )
23		islmhm.m	. . . . . . . . . . . . . 14 |- .x. = ( .s ` S )
24	22, 23	syl6eqr 2674	. . . . . . . . . . . . 13 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( .s ` s ) = .x. )
25	24	oveqd 6667	. . . . . . . . . . . 12 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( x ( .s ` s ) y ) = ( x .x. y ) )
26	25	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( f ` ( x ( .s ` s ) y ) ) = ( f ` ( x .x. y ) ) )
27	5	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( .s ` t ) = ( .s ` T ) )
28		islmhm.n	. . . . . . . . . . . . 13 |- .X. = ( .s ` T )
29	27, 28	syl6eqr 2674	. . . . . . . . . . . 12 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( .s ` t ) = .X. )
30	29	oveqd 6667	. . . . . . . . . . 11 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( x ( .s ` t ) ( f ` y ) ) = ( x .X. ( f ` y ) ) )
31	26, 30	eqeq12d 2637	. . . . . . . . . 10 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) <-> ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) )
32	21, 31	raleqbidv 3152	. . . . . . . . 9 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) <-> A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) )
33	18, 32	raleqbidv 3152	. . . . . . . 8 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) <-> A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) )
34	15, 33	anbi12d 747	. . . . . . 7 |- ( ( ( s = S /\ t = T ) /\ w = (Scalar ` s ) ) -> ( ( (Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) <-> ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) ) )
35	4, 34	sbcied 3472	. . . . . 6 |- ( ( s = S /\ t = T ) -> ( [. (Scalar ` s ) / w ]. ( (Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) <-> ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) ) )
36	3, 35	rabeqbidv 3195	. . . . 5 |- ( ( s = S /\ t = T ) -> { f e. ( s GrpHom t ) | [. (Scalar ` s ) / w ]. ( (Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) } = { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } )
37		ovex 6678	. . . . . 6 |- ( S GrpHom T ) e. _V
38	37	rabex 4813	. . . . 5 |- { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } e. _V
39	36, 1, 38	ovmpt2a 6791	. . . 4 |- ( ( S e. LMod /\ T e. LMod ) -> ( S LMHom T ) = { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } )
40	39	eleq2d 2687	. . 3 |- ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> F e. { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } ) )
41		fveq1 6190	. . . . . . . 8 |- ( f = F -> ( f ` ( x .x. y ) ) = ( F ` ( x .x. y ) ) )
42		fveq1 6190	. . . . . . . . 9 |- ( f = F -> ( f ` y ) = ( F ` y ) )
43	42	oveq2d 6666	. . . . . . . 8 |- ( f = F -> ( x .X. ( f ` y ) ) = ( x .X. ( F ` y ) ) )
44	41, 43	eqeq12d 2637	. . . . . . 7 |- ( f = F -> ( ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) <-> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
45	44	2ralbidv 2989	. . . . . 6 |- ( f = F -> ( A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) <-> A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
46	45	anbi2d 740	. . . . 5 |- ( f = F -> ( ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) <-> ( L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
47	46	elrab 3363	. . . 4 |- ( F e. { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } <-> ( F e. ( S GrpHom T ) /\ ( L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
48		3anass 1042	. . . 4 |- ( ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) <-> ( F e. ( S GrpHom T ) /\ ( L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
49	47, 48	bitr4i 267	. . 3 |- ( F e. { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } <-> ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
50	40, 49	syl6bb 276	. 2 |- ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
51	2, 50	biadan2 674	1 |- ( F e. ( S LMHom T ) <-> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   {crab 2916   _Vcvv 3200   [.wsbc 3435   ` cfv 5888  (class class class)co 6650   Basecbs 15857  Scalarcsca 15944   .scvsca 15945   GrpHom cghm 17657   LModclmod 18863   LMHom clmhm 19019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-lmhm 19022

This theorem is referenced by:  islmhm3  19028  lmhmlem  19029  lmhmlin  19035  islmhmd  19039  reslmhm  19052  lmhmpropd  19073