Metamath Proof Explorer

Theorem rrgsupp

Description: Left multiplication by a left regular element does not change the support set of a vector. (Contributed by Stefan O'Rear, 28-Mar-2015) (Revised by AV, 20-Jul-2019)

Ref Expression
Hypotheses rrgval.e 
|- E = ( RLReg ` R )
rrgval.b 
|- B = ( Base ` R )
rrgval.t 
|- .x. = ( .r ` R )
rrgval.z 
|- .0. = ( 0g ` R )
rrgsupp.i 
|- ( ph -> I e. V )
rrgsupp.r 
|- ( ph -> R e. Ring )
rrgsupp.x 
|- ( ph -> X e. E )
rrgsupp.y 
|- ( ph -> Y : I --> B )
Assertion rrgsupp 
|- ( ph -> ( ( ( I X. { X } ) oF .x. Y ) supp .0. ) = ( Y supp .0. ) )

Proof

Step Hyp Ref Expression
1 rrgval.e 
 |-  E = ( RLReg ` R )
2 rrgval.b 
 |-  B = ( Base ` R )
3 rrgval.t 
 |-  .x. = ( .r ` R )
4 rrgval.z 
 |-  .0. = ( 0g ` R )
5 rrgsupp.i 
 |-  ( ph -> I e. V )
6 rrgsupp.r 
 |-  ( ph -> R e. Ring )
7 rrgsupp.x 
 |-  ( ph -> X e. E )
8 rrgsupp.y 
 |-  ( ph -> Y : I --> B )
9 7 adantr 
 |-  ( ( ph /\ y e. I ) -> X e. E )
10 fvexd 
 |-  ( ( ph /\ y e. I ) -> ( Y ` y ) e. _V )
11 fconstmpt 
 |-  ( I X. { X } ) = ( y e. I |-> X )
12 11 a1i 
 |-  ( ph -> ( I X. { X } ) = ( y e. I |-> X ) )
13 8 feqmptd 
 |-  ( ph -> Y = ( y e. I |-> ( Y ` y ) ) )
14 5 9 10 12 13 offval2 
 |-  ( ph -> ( ( I X. { X } ) oF .x. Y ) = ( y e. I |-> ( X .x. ( Y ` y ) ) ) )
15 14 adantr 
 |-  ( ( ph /\ x e. I ) -> ( ( I X. { X } ) oF .x. Y ) = ( y e. I |-> ( X .x. ( Y ` y ) ) ) )
16 15 fveq1d 
 |-  ( ( ph /\ x e. I ) -> ( ( ( I X. { X } ) oF .x. Y ) ` x ) = ( ( y e. I |-> ( X .x. ( Y ` y ) ) ) ` x ) )
17 simpr 
 |-  ( ( ph /\ x e. I ) -> x e. I )
18 ovex 
 |-  ( X .x. ( Y ` x ) ) e. _V
19 fveq2 
 |-  ( y = x -> ( Y ` y ) = ( Y ` x ) )
20 19 oveq2d 
 |-  ( y = x -> ( X .x. ( Y ` y ) ) = ( X .x. ( Y ` x ) ) )
21 eqid 
 |-  ( y e. I |-> ( X .x. ( Y ` y ) ) ) = ( y e. I |-> ( X .x. ( Y ` y ) ) )
22 20 21 fvmptg 
 |-  ( ( x e. I /\ ( X .x. ( Y ` x ) ) e. _V ) -> ( ( y e. I |-> ( X .x. ( Y ` y ) ) ) ` x ) = ( X .x. ( Y ` x ) ) )
23 17 18 22 sylancl 
 |-  ( ( ph /\ x e. I ) -> ( ( y e. I |-> ( X .x. ( Y ` y ) ) ) ` x ) = ( X .x. ( Y ` x ) ) )
24 16 23 eqtrd 
 |-  ( ( ph /\ x e. I ) -> ( ( ( I X. { X } ) oF .x. Y ) ` x ) = ( X .x. ( Y ` x ) ) )
25 24 neeq1d 
 |-  ( ( ph /\ x e. I ) -> ( ( ( ( I X. { X } ) oF .x. Y ) ` x ) =/= .0. <-> ( X .x. ( Y ` x ) ) =/= .0. ) )
26 25 rabbidva 
 |-  ( ph -> { x e. I | ( ( ( I X. { X } ) oF .x. Y ) ` x ) =/= .0. } = { x e. I | ( X .x. ( Y ` x ) ) =/= .0. } )
27 6 adantr 
 |-  ( ( ph /\ x e. I ) -> R e. Ring )
28 7 adantr 
 |-  ( ( ph /\ x e. I ) -> X e. E )
29 8 ffvelcdmda 
 |-  ( ( ph /\ x e. I ) -> ( Y ` x ) e. B )
30 1 2 3 4 rrgeq0 
 |-  ( ( R e. Ring /\ X e. E /\ ( Y ` x ) e. B ) -> ( ( X .x. ( Y ` x ) ) = .0. <-> ( Y ` x ) = .0. ) )
31 27 28 29 30 syl3anc 
 |-  ( ( ph /\ x e. I ) -> ( ( X .x. ( Y ` x ) ) = .0. <-> ( Y ` x ) = .0. ) )
32 31 necon3bid 
 |-  ( ( ph /\ x e. I ) -> ( ( X .x. ( Y ` x ) ) =/= .0. <-> ( Y ` x ) =/= .0. ) )
33 32 rabbidva 
 |-  ( ph -> { x e. I | ( X .x. ( Y ` x ) ) =/= .0. } = { x e. I | ( Y ` x ) =/= .0. } )
34 26 33 eqtrd 
 |-  ( ph -> { x e. I | ( ( ( I X. { X } ) oF .x. Y ) ` x ) =/= .0. } = { x e. I | ( Y ` x ) =/= .0. } )
35 ovex 
 |-  ( X .x. ( Y ` y ) ) e. _V
36 35 21 fnmpti 
 |-  ( y e. I |-> ( X .x. ( Y ` y ) ) ) Fn I
37 fneq1 
 |-  ( ( ( I X. { X } ) oF .x. Y ) = ( y e. I |-> ( X .x. ( Y ` y ) ) ) -> ( ( ( I X. { X } ) oF .x. Y ) Fn I <-> ( y e. I |-> ( X .x. ( Y ` y ) ) ) Fn I ) )
38 36 37 mpbiri 
 |-  ( ( ( I X. { X } ) oF .x. Y ) = ( y e. I |-> ( X .x. ( Y ` y ) ) ) -> ( ( I X. { X } ) oF .x. Y ) Fn I )
39 14 38 syl 
 |-  ( ph -> ( ( I X. { X } ) oF .x. Y ) Fn I )
40 4 fvexi 
 |-  .0. e. _V
41 40 a1i 
 |-  ( ph -> .0. e. _V )
42 suppvalfn 
 |-  ( ( ( ( I X. { X } ) oF .x. Y ) Fn I /\ I e. V /\ .0. e. _V ) -> ( ( ( I X. { X } ) oF .x. Y ) supp .0. ) = { x e. I | ( ( ( I X. { X } ) oF .x. Y ) ` x ) =/= .0. } )
43 39 5 41 42 syl3anc 
 |-  ( ph -> ( ( ( I X. { X } ) oF .x. Y ) supp .0. ) = { x e. I | ( ( ( I X. { X } ) oF .x. Y ) ` x ) =/= .0. } )
44 8 ffnd 
 |-  ( ph -> Y Fn I )
45 suppvalfn 
 |-  ( ( Y Fn I /\ I e. V /\ .0. e. _V ) -> ( Y supp .0. ) = { x e. I | ( Y ` x ) =/= .0. } )
46 44 5 41 45 syl3anc 
 |-  ( ph -> ( Y supp .0. ) = { x e. I | ( Y ` x ) =/= .0. } )
47 34 43 46 3eqtr4d 
 |-  ( ph -> ( ( ( I X. { X } ) oF .x. Y ) supp .0. ) = ( Y supp .0. ) )