Metamath Proof Explorer

Theorem dprdspan

Description: The direct product is the span of the union of the factors. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypothesis dprdspan.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion dprdspan 
|- ( G dom DProd S -> ( G DProd S ) = ( K ` U. ran S ) )

Proof

Step Hyp Ref Expression
1 dprdspan.k 
 |-  K = ( mrCls ` ( SubGrp ` G ) )
2 id 
 |-  ( G dom DProd S -> G dom DProd S )
3 eqidd 
 |-  ( G dom DProd S -> dom S = dom S )
4 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 5 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
7 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
8 4 6 7 3syl 
 |-  ( G dom DProd S -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
9 dprdf 
 |-  ( G dom DProd S -> S : dom S --> ( SubGrp ` G ) )
10 9 ffnd 
 |-  ( G dom DProd S -> S Fn dom S )
11 fniunfv 
 |-  ( S Fn dom S -> U_ k e. dom S ( S ` k ) = U. ran S )
12 10 11 syl 
 |-  ( G dom DProd S -> U_ k e. dom S ( S ` k ) = U. ran S )
13 simpl 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> G dom DProd S )
14 eqidd 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> dom S = dom S )
15 simpr 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> k e. dom S )
16 13 14 15 dprdub 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> ( S ` k ) C_ ( G DProd S ) )
17 16 ralrimiva 
 |-  ( G dom DProd S -> A. k e. dom S ( S ` k ) C_ ( G DProd S ) )
18 iunss 
 |-  ( U_ k e. dom S ( S ` k ) C_ ( G DProd S ) <-> A. k e. dom S ( S ` k ) C_ ( G DProd S ) )
19 17 18 sylibr 
 |-  ( G dom DProd S -> U_ k e. dom S ( S ` k ) C_ ( G DProd S ) )
20 12 19 eqsstrrd 
 |-  ( G dom DProd S -> U. ran S C_ ( G DProd S ) )
21 5 dprdssv 
 |-  ( G DProd S ) C_ ( Base ` G )
22 20 21 sstrdi 
 |-  ( G dom DProd S -> U. ran S C_ ( Base ` G ) )
23 1 mrccl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ran S C_ ( Base ` G ) ) -> ( K ` U. ran S ) e. ( SubGrp ` G ) )
24 8 22 23 syl2anc 
 |-  ( G dom DProd S -> ( K ` U. ran S ) e. ( SubGrp ` G ) )
25 eqimss 
 |-  ( U_ k e. dom S ( S ` k ) = U. ran S -> U_ k e. dom S ( S ` k ) C_ U. ran S )
26 12 25 syl 
 |-  ( G dom DProd S -> U_ k e. dom S ( S ` k ) C_ U. ran S )
27 iunss 
 |-  ( U_ k e. dom S ( S ` k ) C_ U. ran S <-> A. k e. dom S ( S ` k ) C_ U. ran S )
28 26 27 sylib 
 |-  ( G dom DProd S -> A. k e. dom S ( S ` k ) C_ U. ran S )
29 28 r19.21bi 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> ( S ` k ) C_ U. ran S )
30 8 1 22 mrcssidd 
 |-  ( G dom DProd S -> U. ran S C_ ( K ` U. ran S ) )
31 30 adantr 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> U. ran S C_ ( K ` U. ran S ) )
32 29 31 sstrd 
 |-  ( ( G dom DProd S /\ k e. dom S ) -> ( S ` k ) C_ ( K ` U. ran S ) )
33 2 3 24 32 dprdlub 
 |-  ( G dom DProd S -> ( G DProd S ) C_ ( K ` U. ran S ) )
34 dprdsubg 
 |-  ( G dom DProd S -> ( G DProd S ) e. ( SubGrp ` G ) )
35 1 mrcsscl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ran S C_ ( G DProd S ) /\ ( G DProd S ) e. ( SubGrp ` G ) ) -> ( K ` U. ran S ) C_ ( G DProd S ) )
36 8 20 34 35 syl3anc 
 |-  ( G dom DProd S -> ( K ` U. ran S ) C_ ( G DProd S ) )
37 33 36 eqssd 
 |-  ( G dom DProd S -> ( G DProd S ) = ( K ` U. ran S ) )