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 ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion dprdspan ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) = ( 𝐾 ‘ ∪ ran 𝑆 ) )

Proof

Step Hyp Ref Expression
1 dprdspan.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
2 id ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 dom DProd 𝑆 )
3 eqidd ⊢ ( 𝐺 dom DProd 𝑆 → dom 𝑆 = dom 𝑆 )
4 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
5 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 5 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
7 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
8 4 6 7 3syl ⊢ ( 𝐺 dom DProd 𝑆 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
9 dprdf ⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) )
10 9 ffnd ⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 Fn dom 𝑆 )
11 fniunfv ⊢ ( 𝑆 Fn dom 𝑆 → ∪ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) = ∪ ran 𝑆 )
12 10 11 syl ⊢ ( 𝐺 dom DProd 𝑆 → ∪ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) = ∪ ran 𝑆 )
13 simpl ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → 𝐺 dom DProd 𝑆 )
14 eqidd ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → dom 𝑆 = dom 𝑆 )
15 simpr ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → 𝑘 ∈ dom 𝑆 )
16 13 14 15 dprdub ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝐺 DProd 𝑆 ) )
17 16 ralrimiva ⊢ ( 𝐺 dom DProd 𝑆 → ∀ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝐺 DProd 𝑆 ) )
18 iunss ⊢ ( ∪ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝐺 DProd 𝑆 ) ↔ ∀ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝐺 DProd 𝑆 ) )
19 17 18 sylibr ⊢ ( 𝐺 dom DProd 𝑆 → ∪ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝐺 DProd 𝑆 ) )
20 12 19 eqsstrrd ⊢ ( 𝐺 dom DProd 𝑆 → ∪ ran 𝑆 ⊆ ( 𝐺 DProd 𝑆 ) )
21 5 dprdssv ⊢ ( 𝐺 DProd 𝑆 ) ⊆ ( Base ‘ 𝐺 )
22 20 21 sstrdi ⊢ ( 𝐺 dom DProd 𝑆 → ∪ ran 𝑆 ⊆ ( Base ‘ 𝐺 ) )
23 1 mrccl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ran 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝐾 ‘ ∪ ran 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )
24 8 22 23 syl2anc ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐾 ‘ ∪ ran 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )
25 eqimss ⊢ ( ∪ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) = ∪ ran 𝑆 → ∪ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) ⊆ ∪ ran 𝑆 )
26 12 25 syl ⊢ ( 𝐺 dom DProd 𝑆 → ∪ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) ⊆ ∪ ran 𝑆 )
27 iunss ⊢ ( ∪ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) ⊆ ∪ ran 𝑆 ↔ ∀ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) ⊆ ∪ ran 𝑆 )
28 26 27 sylib ⊢ ( 𝐺 dom DProd 𝑆 → ∀ 𝑘 ∈ dom 𝑆 ( 𝑆 ‘ 𝑘 ) ⊆ ∪ ran 𝑆 )
29 28 r19.21bi ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ∪ ran 𝑆 )
30 8 1 22 mrcssidd ⊢ ( 𝐺 dom DProd 𝑆 → ∪ ran 𝑆 ⊆ ( 𝐾 ‘ ∪ ran 𝑆 ) )
31 30 adantr ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → ∪ ran 𝑆 ⊆ ( 𝐾 ‘ ∪ ran 𝑆 ) )
32 29 31 sstrd ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝐾 ‘ ∪ ran 𝑆 ) )
33 2 3 24 32 dprdlub ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) ⊆ ( 𝐾 ‘ ∪ ran 𝑆 ) )
34 dprdsubg ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )
35 1 mrcsscl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ran 𝑆 ⊆ ( 𝐺 DProd 𝑆 ) ∧ ( 𝐺 DProd 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐾 ‘ ∪ ran 𝑆 ) ⊆ ( 𝐺 DProd 𝑆 ) )
36 8 20 34 35 syl3anc ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐾 ‘ ∪ ran 𝑆 ) ⊆ ( 𝐺 DProd 𝑆 ) )
37 33 36 eqssd ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) = ( 𝐾 ‘ ∪ ran 𝑆 ) )