Metamath Proof Explorer

Theorem dprdub

Description: Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdub.1 
|- ( ph -> G dom DProd S )
dprdub.2 
|- ( ph -> dom S = I )
dprdub.3 
|- ( ph -> X e. I )
Assertion dprdub 
|- ( ph -> ( S ` X ) C_ ( G DProd S ) )

Proof

Step Hyp Ref Expression
1 dprdub.1 
 |-  ( ph -> G dom DProd S )
2 dprdub.2 
 |-  ( ph -> dom S = I )
3 dprdub.3 
 |-  ( ph -> X e. I )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 eqid 
 |-  { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } = { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) }
6 1 adantr 
 |-  ( ( ph /\ x e. ( S ` X ) ) -> G dom DProd S )
7 2 adantr 
 |-  ( ( ph /\ x e. ( S ` X ) ) -> dom S = I )
8 3 adantr 
 |-  ( ( ph /\ x e. ( S ` X ) ) -> X e. I )
9 simpr 
 |-  ( ( ph /\ x e. ( S ` X ) ) -> x e. ( S ` X ) )
10 eqid 
 |-  ( n e. I |-> if ( n = X , x , ( 0g ` G ) ) ) = ( n e. I |-> if ( n = X , x , ( 0g ` G ) ) )
11 4 5 6 7 8 9 10 dprdfid 
 |-  ( ( ph /\ x e. ( S ` X ) ) -> ( ( n e. I |-> if ( n = X , x , ( 0g ` G ) ) ) e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } /\ ( G gsum ( n e. I |-> if ( n = X , x , ( 0g ` G ) ) ) ) = x ) )
12 11 simprd 
 |-  ( ( ph /\ x e. ( S ` X ) ) -> ( G gsum ( n e. I |-> if ( n = X , x , ( 0g ` G ) ) ) ) = x )
13 11 simpld 
 |-  ( ( ph /\ x e. ( S ` X ) ) -> ( n e. I |-> if ( n = X , x , ( 0g ` G ) ) ) e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } )
14 4 5 6 7 13 eldprdi 
 |-  ( ( ph /\ x e. ( S ` X ) ) -> ( G gsum ( n e. I |-> if ( n = X , x , ( 0g ` G ) ) ) ) e. ( G DProd S ) )
15 12 14 eqeltrrd 
 |-  ( ( ph /\ x e. ( S ` X ) ) -> x e. ( G DProd S ) )
16 15 ex 
 |-  ( ph -> ( x e. ( S ` X ) -> x e. ( G DProd S ) ) )
17 16 ssrdv 
 |-  ( ph -> ( S ` X ) C_ ( G DProd S ) )