Metamath Proof Explorer

Theorem lmhmeql

Description: The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypothesis lmhmeql.u 
|- U = ( LSubSp ` S )
Assertion lmhmeql 
|- ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> dom ( F i^i G ) e. U )

Proof

Step Hyp Ref Expression
1 lmhmeql.u 
 |-  U = ( LSubSp ` S )
2 lmghm 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
3 lmghm 
 |-  ( G e. ( S LMHom T ) -> G e. ( S GrpHom T ) )
4 ghmeql 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> dom ( F i^i G ) e. ( SubGrp ` S ) )
5 2 3 4 syl2an 
 |-  ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> dom ( F i^i G ) e. ( SubGrp ` S ) )
6 fveq2 
 |-  ( z = ( x ( .s ` S ) y ) -> ( F ` z ) = ( F ` ( x ( .s ` S ) y ) ) )
7 fveq2 
 |-  ( z = ( x ( .s ` S ) y ) -> ( G ` z ) = ( G ` ( x ( .s ` S ) y ) ) )
8 6 7 eqeq12d 
 |-  ( z = ( x ( .s ` S ) y ) -> ( ( F ` z ) = ( G ` z ) <-> ( F ` ( x ( .s ` S ) y ) ) = ( G ` ( x ( .s ` S ) y ) ) ) )
9 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
10 9 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> S e. LMod )
11 10 ad2antrr 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> S e. LMod )
12 simplr 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> x e. ( Base ` ( Scalar ` S ) ) )
13 simprl 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> y e. ( Base ` S ) )
14 eqid 
 |-  ( Base ` S ) = ( Base ` S )
15 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
16 eqid 
 |-  ( .s ` S ) = ( .s ` S )
17 eqid 
 |-  ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
18 14 15 16 17 lmodvscl 
 |-  ( ( S e. LMod /\ x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) -> ( x ( .s ` S ) y ) e. ( Base ` S ) )
19 11 12 13 18 syl3anc 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( x ( .s ` S ) y ) e. ( Base ` S ) )
20 oveq2 
 |-  ( ( F ` y ) = ( G ` y ) -> ( x ( .s ` T ) ( F ` y ) ) = ( x ( .s ` T ) ( G ` y ) ) )
21 20 ad2antll 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( x ( .s ` T ) ( F ` y ) ) = ( x ( .s ` T ) ( G ` y ) ) )
22 simplll 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> F e. ( S LMHom T ) )
23 eqid 
 |-  ( .s ` T ) = ( .s ` T )
24 15 17 14 16 23 lmhmlin 
 |-  ( ( F e. ( S LMHom T ) /\ x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` T ) ( F ` y ) ) )
25 22 12 13 24 syl3anc 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( x ( .s ` T ) ( F ` y ) ) )
26 simpllr 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> G e. ( S LMHom T ) )
27 15 17 14 16 23 lmhmlin 
 |-  ( ( G e. ( S LMHom T ) /\ x e. ( Base ` ( Scalar ` S ) ) /\ y e. ( Base ` S ) ) -> ( G ` ( x ( .s ` S ) y ) ) = ( x ( .s ` T ) ( G ` y ) ) )
28 26 12 13 27 syl3anc 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( G ` ( x ( .s ` S ) y ) ) = ( x ( .s ` T ) ( G ` y ) ) )
29 21 25 28 3eqtr4d 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( F ` ( x ( .s ` S ) y ) ) = ( G ` ( x ( .s ` S ) y ) ) )
30 8 19 29 elrabd 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( x ( .s ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
31 30 expr 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) /\ y e. ( Base ` S ) ) -> ( ( F ` y ) = ( G ` y ) -> ( x ( .s ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
32 31 ralrimiva 
 |-  ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) -> A. y e. ( Base ` S ) ( ( F ` y ) = ( G ` y ) -> ( x ( .s ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
33 eqid 
 |-  ( Base ` T ) = ( Base ` T )
34 14 33 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
35 34 ffnd 
 |-  ( F e. ( S LMHom T ) -> F Fn ( Base ` S ) )
36 14 33 lmhmf 
 |-  ( G e. ( S LMHom T ) -> G : ( Base ` S ) --> ( Base ` T ) )
37 36 ffnd 
 |-  ( G e. ( S LMHom T ) -> G Fn ( Base ` S ) )
38 fndmin 
 |-  ( ( F Fn ( Base ` S ) /\ G Fn ( Base ` S ) ) -> dom ( F i^i G ) = { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
39 35 37 38 syl2an 
 |-  ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> dom ( F i^i G ) = { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
40 39 adantr 
 |-  ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) -> dom ( F i^i G ) = { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
41 eleq2 
 |-  ( dom ( F i^i G ) = { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } -> ( ( x ( .s ` S ) y ) e. dom ( F i^i G ) <-> ( x ( .s ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
42 41 raleqbi1dv 
 |-  ( dom ( F i^i G ) = { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } -> ( A. y e. dom ( F i^i G ) ( x ( .s ` S ) y ) e. dom ( F i^i G ) <-> A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( .s ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
43 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
44 fveq2 
 |-  ( z = y -> ( G ` z ) = ( G ` y ) )
45 43 44 eqeq12d 
 |-  ( z = y -> ( ( F ` z ) = ( G ` z ) <-> ( F ` y ) = ( G ` y ) ) )
46 45 ralrab 
 |-  ( A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( .s ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } <-> A. y e. ( Base ` S ) ( ( F ` y ) = ( G ` y ) -> ( x ( .s ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
47 42 46 bitrdi 
 |-  ( dom ( F i^i G ) = { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } -> ( A. y e. dom ( F i^i G ) ( x ( .s ` S ) y ) e. dom ( F i^i G ) <-> A. y e. ( Base ` S ) ( ( F ` y ) = ( G ` y ) -> ( x ( .s ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) ) )
48 40 47 syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) -> ( A. y e. dom ( F i^i G ) ( x ( .s ` S ) y ) e. dom ( F i^i G ) <-> A. y e. ( Base ` S ) ( ( F ` y ) = ( G ` y ) -> ( x ( .s ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) ) )
49 32 48 mpbird 
 |-  ( ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) /\ x e. ( Base ` ( Scalar ` S ) ) ) -> A. y e. dom ( F i^i G ) ( x ( .s ` S ) y ) e. dom ( F i^i G ) )
50 49 ralrimiva 
 |-  ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> A. x e. ( Base ` ( Scalar ` S ) ) A. y e. dom ( F i^i G ) ( x ( .s ` S ) y ) e. dom ( F i^i G ) )
51 15 17 14 16 1 islss4 
 |-  ( S e. LMod -> ( dom ( F i^i G ) e. U <-> ( dom ( F i^i G ) e. ( SubGrp ` S ) /\ A. x e. ( Base ` ( Scalar ` S ) ) A. y e. dom ( F i^i G ) ( x ( .s ` S ) y ) e. dom ( F i^i G ) ) ) )
52 10 51 syl 
 |-  ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> ( dom ( F i^i G ) e. U <-> ( dom ( F i^i G ) e. ( SubGrp ` S ) /\ A. x e. ( Base ` ( Scalar ` S ) ) A. y e. dom ( F i^i G ) ( x ( .s ` S ) y ) e. dom ( F i^i G ) ) ) )
53 5 50 52 mpbir2and 
 |-  ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> dom ( F i^i G ) e. U )