Metamath Proof Explorer

Theorem dsmmbas2

Description: Base set of the direct sum module using the fndmin abbreviation. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses dsmmbas2.p 
|- P = ( S Xs_ R )
dsmmbas2.b 
|- B = { f e. ( Base ` P ) | dom ( f \ ( 0g o. R ) ) e. Fin }
Assertion dsmmbas2 
|- ( ( R Fn I /\ I e. V ) -> B = ( Base ` ( S (+)m R ) ) )

Proof

Step Hyp Ref Expression
1 dsmmbas2.p 
 |-  P = ( S Xs_ R )
2 dsmmbas2.b 
 |-  B = { f e. ( Base ` P ) | dom ( f \ ( 0g o. R ) ) e. Fin }
3 1 fveq2i 
 |-  ( Base ` P ) = ( Base ` ( S Xs_ R ) )
4 3 rabeqi 
 |-  { f e. ( Base ` P ) | dom ( f \ ( 0g o. R ) ) e. Fin } = { f e. ( Base ` ( S Xs_ R ) ) | dom ( f \ ( 0g o. R ) ) e. Fin }
5 simpll 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> R Fn I )
6 fvco2 
 |-  ( ( R Fn I /\ x e. I ) -> ( ( 0g o. R ) ` x ) = ( 0g ` ( R ` x ) ) )
7 5 6 sylan 
 |-  ( ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) /\ x e. I ) -> ( ( 0g o. R ) ` x ) = ( 0g ` ( R ` x ) ) )
8 7 neeq2d 
 |-  ( ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) /\ x e. I ) -> ( ( f ` x ) =/= ( ( 0g o. R ) ` x ) <-> ( f ` x ) =/= ( 0g ` ( R ` x ) ) ) )
9 8 rabbidva 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> { x e. I | ( f ` x ) =/= ( ( 0g o. R ) ` x ) } = { x e. I | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } )
10 eqid 
 |-  ( S Xs_ R ) = ( S Xs_ R )
11 eqid 
 |-  ( Base ` ( S Xs_ R ) ) = ( Base ` ( S Xs_ R ) )
12 reldmprds 
 |-  Rel dom Xs_
13 10 11 12 strov2rcl 
 |-  ( f e. ( Base ` ( S Xs_ R ) ) -> S e. _V )
14 13 adantl 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> S e. _V )
15 simplr 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> I e. V )
16 simpr 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> f e. ( Base ` ( S Xs_ R ) ) )
17 10 11 14 15 5 16 prdsbasfn 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> f Fn I )
18 fn0g 
 |-  0g Fn _V
19 dffn2 
 |-  ( 0g Fn _V <-> 0g : _V --> _V )
20 18 19 mpbi 
 |-  0g : _V --> _V
21 dffn2 
 |-  ( R Fn I <-> R : I --> _V )
22 21 biimpi 
 |-  ( R Fn I -> R : I --> _V )
23 fco 
 |-  ( ( 0g : _V --> _V /\ R : I --> _V ) -> ( 0g o. R ) : I --> _V )
24 20 22 23 sylancr 
 |-  ( R Fn I -> ( 0g o. R ) : I --> _V )
25 24 ffnd 
 |-  ( R Fn I -> ( 0g o. R ) Fn I )
26 5 25 syl 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> ( 0g o. R ) Fn I )
27 fndmdif 
 |-  ( ( f Fn I /\ ( 0g o. R ) Fn I ) -> dom ( f \ ( 0g o. R ) ) = { x e. I | ( f ` x ) =/= ( ( 0g o. R ) ` x ) } )
28 17 26 27 syl2anc 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> dom ( f \ ( 0g o. R ) ) = { x e. I | ( f ` x ) =/= ( ( 0g o. R ) ` x ) } )
29 fndm 
 |-  ( R Fn I -> dom R = I )
30 29 rabeqdv 
 |-  ( R Fn I -> { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } = { x e. I | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } )
31 5 30 syl 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } = { x e. I | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } )
32 9 28 31 3eqtr4d 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> dom ( f \ ( 0g o. R ) ) = { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } )
33 32 eleq1d 
 |-  ( ( ( R Fn I /\ I e. V ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> ( dom ( f \ ( 0g o. R ) ) e. Fin <-> { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin ) )
34 33 rabbidva 
 |-  ( ( R Fn I /\ I e. V ) -> { f e. ( Base ` ( S Xs_ R ) ) | dom ( f \ ( 0g o. R ) ) e. Fin } = { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } )
35 4 34 syl5eq 
 |-  ( ( R Fn I /\ I e. V ) -> { f e. ( Base ` P ) | dom ( f \ ( 0g o. R ) ) e. Fin } = { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } )
36 fnex 
 |-  ( ( R Fn I /\ I e. V ) -> R e. _V )
37 eqid 
 |-  { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } = { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin }
38 37 dsmmbase 
 |-  ( R e. _V -> { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } = ( Base ` ( S (+)m R ) ) )
39 36 38 syl 
 |-  ( ( R Fn I /\ I e. V ) -> { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } = ( Base ` ( S (+)m R ) ) )
40 35 39 eqtrd 
 |-  ( ( R Fn I /\ I e. V ) -> { f e. ( Base ` P ) | dom ( f \ ( 0g o. R ) ) e. Fin } = ( Base ` ( S (+)m R ) ) )
41 2 40 syl5eq 
 |-  ( ( R Fn I /\ I e. V ) -> B = ( Base ` ( S (+)m R ) ) )