Metamath Proof Explorer

Theorem lincext1

Description: Property 1 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019) (Revised by AV, 29-Apr-2019)

Ref Expression
Hypotheses lincext.b 
|- B = ( Base ` M )
lincext.r 
|- R = ( Scalar ` M )
lincext.e 
|- E = ( Base ` R )
lincext.0 
|- .0. = ( 0g ` R )
lincext.z 
|- Z = ( 0g ` M )
lincext.n 
|- N = ( invg ` R )
lincext.f 
|- F = ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) )
Assertion lincext1 
|- ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> F e. ( E ^m S ) )

Proof

Step Hyp Ref Expression
1 lincext.b 
 |-  B = ( Base ` M )
2 lincext.r 
 |-  R = ( Scalar ` M )
3 lincext.e 
 |-  E = ( Base ` R )
4 lincext.0 
 |-  .0. = ( 0g ` R )
5 lincext.z 
 |-  Z = ( 0g ` M )
6 lincext.n 
 |-  N = ( invg ` R )
7 lincext.f 
 |-  F = ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) )
8 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
9 8 lmodfgrp 
 |-  ( M e. LMod -> ( Scalar ` M ) e. Grp )
10 9 ad2antrr 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( Scalar ` M ) e. Grp )
11 2 10 eqeltrid 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> R e. Grp )
12 simpr1 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> Y e. E )
13 3 6 grpinvcl 
 |-  ( ( R e. Grp /\ Y e. E ) -> ( N ` Y ) e. E )
14 11 12 13 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( N ` Y ) e. E )
15 14 ad2antrr 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) /\ z e. S ) /\ z = X ) -> ( N ` Y ) e. E )
16 elmapi 
 |-  ( G e. ( E ^m ( S \ { X } ) ) -> G : ( S \ { X } ) --> E )
17 df-ne 
 |-  ( z =/= X <-> -. z = X )
18 17 biimpri 
 |-  ( -. z = X -> z =/= X )
19 18 anim2i 
 |-  ( ( z e. S /\ -. z = X ) -> ( z e. S /\ z =/= X ) )
20 eldifsn 
 |-  ( z e. ( S \ { X } ) <-> ( z e. S /\ z =/= X ) )
21 19 20 sylibr 
 |-  ( ( z e. S /\ -. z = X ) -> z e. ( S \ { X } ) )
22 ffvelrn 
 |-  ( ( G : ( S \ { X } ) --> E /\ z e. ( S \ { X } ) ) -> ( G ` z ) e. E )
23 21 22 sylan2 
 |-  ( ( G : ( S \ { X } ) --> E /\ ( z e. S /\ -. z = X ) ) -> ( G ` z ) e. E )
24 23 ex 
 |-  ( G : ( S \ { X } ) --> E -> ( ( z e. S /\ -. z = X ) -> ( G ` z ) e. E ) )
25 16 24 syl 
 |-  ( G e. ( E ^m ( S \ { X } ) ) -> ( ( z e. S /\ -. z = X ) -> ( G ` z ) e. E ) )
26 25 3ad2ant3 
 |-  ( ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) -> ( ( z e. S /\ -. z = X ) -> ( G ` z ) e. E ) )
27 26 adantl 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( ( z e. S /\ -. z = X ) -> ( G ` z ) e. E ) )
28 27 impl 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) /\ z e. S ) /\ -. z = X ) -> ( G ` z ) e. E )
29 15 28 ifclda 
 |-  ( ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) /\ z e. S ) -> if ( z = X , ( N ` Y ) , ( G ` z ) ) e. E )
30 29 fmpttd 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) ) : S --> E )
31 simpr 
 |-  ( ( M e. LMod /\ S e. ~P B ) -> S e. ~P B )
32 3 fvexi 
 |-  E e. _V
33 31 32 jctil 
 |-  ( ( M e. LMod /\ S e. ~P B ) -> ( E e. _V /\ S e. ~P B ) )
34 33 adantr 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( E e. _V /\ S e. ~P B ) )
35 elmapg 
 |-  ( ( E e. _V /\ S e. ~P B ) -> ( ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) ) e. ( E ^m S ) <-> ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) ) : S --> E ) )
36 34 35 syl 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) ) e. ( E ^m S ) <-> ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) ) : S --> E ) )
37 30 36 mpbird 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) ) e. ( E ^m S ) )
38 7 37 eqeltrid 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> F e. ( E ^m S ) )