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

Metamath Proof Explorer

Theorem dprdlub

Description: The direct product is smaller than any subgroup which contains the factors. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdlub.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dprdlub.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dprdlub.3 ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
dprdlub.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑘 ) ⊆ 𝑇 )
Assertion dprdlub ( 𝜑 → ( 𝐺 DProd 𝑆 ) ⊆ 𝑇 )

Proof

Step Hyp Ref Expression
1 dprdlub.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dprdlub.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dprdlub.3 ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
4 dprdlub.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑘 ) ⊆ 𝑇 )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 eqid ⊢ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) }
7 5 6 dprdval ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ↦ ( 𝐺 Σg 𝑓 ) ) )
8 1 2 7 syl2anc ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ↦ ( 𝐺 Σg 𝑓 ) ) )
9 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 dom DProd 𝑆 )
11 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
12 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
13 10 11 12 3syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 ∈ Mnd )
14 1 2 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐼 ∈ V )
16 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
17 subgsubm ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ∈ ( SubMnd ‘ 𝐺 ) )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑇 ∈ ( SubMnd ‘ 𝐺 ) )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → dom 𝑆 = 𝐼 )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
21 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
22 6 10 19 20 21 dprdff ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
23 22 ffnd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 Fn 𝐼 )
24 4 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑘 ) ⊆ 𝑇 )
25 6 10 19 20 dprdfcl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
26 24 25 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝑇 )
27 26 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ∀ 𝑘 ∈ 𝐼 ( 𝑓 ‘ 𝑘 ) ∈ 𝑇 )
28 ffnfv ⊢ ( 𝑓 : 𝐼 ⟶ 𝑇 ↔ ( 𝑓 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑓 ‘ 𝑘 ) ∈ 𝑇 ) )
29 23 27 28 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 : 𝐼 ⟶ 𝑇 )
30 6 10 19 20 9 dprdfcntz ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ran 𝑓 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝑓 ) )
31 6 10 19 20 dprdffsupp ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 finSupp ( 0g ‘ 𝐺 ) )
32 5 9 13 15 18 29 30 31 gsumzsubmcl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ( 𝐺 Σg 𝑓 ) ∈ 𝑇 )
33 32 fmpttd ⊢ ( 𝜑 → ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ↦ ( 𝐺 Σg 𝑓 ) ) : { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ⟶ 𝑇 )
34 33 frnd ⊢ ( 𝜑 → ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ↦ ( 𝐺 Σg 𝑓 ) ) ⊆ 𝑇 )
35 8 34 eqsstrd ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) ⊆ 𝑇 )