Metamath Proof Explorer

Theorem dprdsn

Description: A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Assertion dprdsn 
|- ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ( G dom DProd { <. A , S >. } /\ ( G DProd { <. A , S >. } ) = S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
2 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
3 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
4 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
5 4 adantl 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> G e. Grp )
6 snex 
 |-  { A } e. _V
7 6 a1i 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> { A } e. _V )
8 f1osng 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> { <. A , S >. } : { A } -1-1-onto-> { S } )
9 f1of 
 |-  ( { <. A , S >. } : { A } -1-1-onto-> { S } -> { <. A , S >. } : { A } --> { S } )
10 8 9 syl 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> { <. A , S >. } : { A } --> { S } )
11 simpr 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> S e. ( SubGrp ` G ) )
12 11 snssd 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> { S } C_ ( SubGrp ` G ) )
13 10 12 fssd 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> { <. A , S >. } : { A } --> ( SubGrp ` G ) )
14 simpr1 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ ( x e. { A } /\ y e. { A } /\ x =/= y ) ) -> x e. { A } )
15 elsni 
 |-  ( x e. { A } -> x = A )
16 14 15 syl 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ ( x e. { A } /\ y e. { A } /\ x =/= y ) ) -> x = A )
17 simpr2 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ ( x e. { A } /\ y e. { A } /\ x =/= y ) ) -> y e. { A } )
18 elsni 
 |-  ( y e. { A } -> y = A )
19 17 18 syl 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ ( x e. { A } /\ y e. { A } /\ x =/= y ) ) -> y = A )
20 16 19 eqtr4d 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ ( x e. { A } /\ y e. { A } /\ x =/= y ) ) -> x = y )
21 simpr3 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ ( x e. { A } /\ y e. { A } /\ x =/= y ) ) -> x =/= y )
22 20 21 pm2.21ddne 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ ( x e. { A } /\ y e. { A } /\ x =/= y ) ) -> ( { <. A , S >. } ` x ) C_ ( ( Cntz ` G ) ` ( { <. A , S >. } ` y ) ) )
23 5 adantr 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> G e. Grp )
24 eqid 
 |-  ( Base ` G ) = ( Base ` G )
25 24 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
26 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
27 23 25 26 3syl 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
28 15 adantl 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> x = A )
29 28 sneqd 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> { x } = { A } )
30 29 difeq2d 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( { A } \ { x } ) = ( { A } \ { A } ) )
31 difid 
 |-  ( { A } \ { A } ) = (/)
32 30 31 eqtrdi 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( { A } \ { x } ) = (/) )
33 32 imaeq2d 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( { <. A , S >. } " ( { A } \ { x } ) ) = ( { <. A , S >. } " (/) ) )
34 ima0 
 |-  ( { <. A , S >. } " (/) ) = (/)
35 33 34 eqtrdi 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( { <. A , S >. } " ( { A } \ { x } ) ) = (/) )
36 35 unieqd 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> U. ( { <. A , S >. } " ( { A } \ { x } ) ) = U. (/) )
37 uni0 
 |-  U. (/) = (/)
38 36 37 eqtrdi 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> U. ( { <. A , S >. } " ( { A } \ { x } ) ) = (/) )
39 0ss 
 |-  (/) C_ { ( 0g ` G ) }
40 39 a1i 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> (/) C_ { ( 0g ` G ) } )
41 38 40 eqsstrd 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> U. ( { <. A , S >. } " ( { A } \ { x } ) ) C_ { ( 0g ` G ) } )
42 2 0subg 
 |-  ( G e. Grp -> { ( 0g ` G ) } e. ( SubGrp ` G ) )
43 23 42 syl 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> { ( 0g ` G ) } e. ( SubGrp ` G ) )
44 3 mrcsscl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( { <. A , S >. } " ( { A } \ { x } ) ) C_ { ( 0g ` G ) } /\ { ( 0g ` G ) } e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( { <. A , S >. } " ( { A } \ { x } ) ) ) C_ { ( 0g ` G ) } )
45 27 41 43 44 syl3anc 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( { <. A , S >. } " ( { A } \ { x } ) ) ) C_ { ( 0g ` G ) } )
46 2 subg0cl 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` G ) e. S )
47 46 ad2antlr 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( 0g ` G ) e. S )
48 15 fveq2d 
 |-  ( x e. { A } -> ( { <. A , S >. } ` x ) = ( { <. A , S >. } ` A ) )
49 fvsng 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ( { <. A , S >. } ` A ) = S )
50 48 49 sylan9eqr 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( { <. A , S >. } ` x ) = S )
51 47 50 eleqtrrd 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( 0g ` G ) e. ( { <. A , S >. } ` x ) )
52 51 snssd 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> { ( 0g ` G ) } C_ ( { <. A , S >. } ` x ) )
53 45 52 sstrd 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( { <. A , S >. } " ( { A } \ { x } ) ) ) C_ ( { <. A , S >. } ` x ) )
54 sseqin2 
 |-  ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( { <. A , S >. } " ( { A } \ { x } ) ) ) C_ ( { <. A , S >. } ` x ) <-> ( ( { <. A , S >. } ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( { <. A , S >. } " ( { A } \ { x } ) ) ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( { <. A , S >. } " ( { A } \ { x } ) ) ) )
55 53 54 sylib 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( ( { <. A , S >. } ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( { <. A , S >. } " ( { A } \ { x } ) ) ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( { <. A , S >. } " ( { A } \ { x } ) ) ) )
56 55 45 eqsstrd 
 |-  ( ( ( A e. V /\ S e. ( SubGrp ` G ) ) /\ x e. { A } ) -> ( ( { <. A , S >. } ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( { <. A , S >. } " ( { A } \ { x } ) ) ) ) C_ { ( 0g ` G ) } )
57 1 2 3 5 7 13 22 56 dmdprdd 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> G dom DProd { <. A , S >. } )
58 3 dprdspan 
 |-  ( G dom DProd { <. A , S >. } -> ( G DProd { <. A , S >. } ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran { <. A , S >. } ) )
59 57 58 syl 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ( G DProd { <. A , S >. } ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran { <. A , S >. } ) )
60 rnsnopg 
 |-  ( A e. V -> ran { <. A , S >. } = { S } )
61 60 adantr 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ran { <. A , S >. } = { S } )
62 61 unieqd 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> U. ran { <. A , S >. } = U. { S } )
63 unisng 
 |-  ( S e. ( SubGrp ` G ) -> U. { S } = S )
64 63 adantl 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> U. { S } = S )
65 62 64 eqtrd 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> U. ran { <. A , S >. } = S )
66 65 fveq2d 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran { <. A , S >. } ) = ( ( mrCls ` ( SubGrp ` G ) ) ` S ) )
67 5 25 26 3syl 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
68 3 mrcid 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ S e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` S ) = S )
69 67 68 sylancom 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` S ) = S )
70 66 69 eqtrd 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran { <. A , S >. } ) = S )
71 59 70 eqtrd 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ( G DProd { <. A , S >. } ) = S )
72 57 71 jca 
 |-  ( ( A e. V /\ S e. ( SubGrp ` G ) ) -> ( G dom DProd { <. A , S >. } /\ ( G DProd { <. A , S >. } ) = S ) )