This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dprdssv

Description: The internal direct product of a family of subgroups is a subset of the base. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypothesis dprdssv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion dprdssv ( 𝐺 DProd 𝑆 ) ⊆ 𝐵

Proof

Step Hyp Ref Expression
1 dprdssv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 eqid ⊢ dom 𝑆 = dom 𝑆
3 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
4 eqid ⊢ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } = { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) }
5 3 4 eldprd ⊢ ( dom 𝑆 = dom 𝑆 → ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ) ) )
6 2 5 ax-mp ⊢ ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ) )
7 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
8 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
9 8 grpmndd ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Mnd )
10 9 adantr ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 ∈ Mnd )
11 reldmdprd ⊢ Rel dom DProd
12 11 brrelex2i ⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 ∈ V )
13 12 dmexd ⊢ ( 𝐺 dom DProd 𝑆 → dom 𝑆 ∈ V )
14 13 adantr ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → dom 𝑆 ∈ V )
15 simpl ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 dom DProd 𝑆 )
16 eqidd ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → dom 𝑆 = dom 𝑆 )
17 simpr ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
18 4 15 16 17 1 dprdff ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 : dom 𝑆 ⟶ 𝐵 )
19 4 15 16 17 7 dprdfcntz ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ran 𝑓 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝑓 ) )
20 4 15 16 17 dprdffsupp ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 finSupp ( 0g ‘ 𝐺 ) )
21 1 3 7 10 14 18 19 20 gsumzcl ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ( 𝐺 Σg 𝑓 ) ∈ 𝐵 )
22 eleq1 ⊢ ( 𝑥 = ( 𝐺 Σg 𝑓 ) → ( 𝑥 ∈ 𝐵 ↔ ( 𝐺 Σg 𝑓 ) ∈ 𝐵 ) )
23 21 22 syl5ibrcom ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ( 𝑥 = ( 𝐺 Σg 𝑓 ) → 𝑥 ∈ 𝐵 ) )
24 23 rexlimdva ⊢ ( 𝐺 dom DProd 𝑆 → ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) → 𝑥 ∈ 𝐵 ) )
25 24 imp ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ) → 𝑥 ∈ 𝐵 )
26 6 25 sylbi ⊢ ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) → 𝑥 ∈ 𝐵 )
27 26 ssriv ⊢ ( 𝐺 DProd 𝑆 ) ⊆ 𝐵