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

Metamath Proof Explorer

Theorem dprdub

Description: Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdub.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dprdub.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dprdub.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion dprdub ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝐺 DProd 𝑆 ) )

Proof

Step Hyp Ref Expression
1 dprdub.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dprdub.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dprdub.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
4 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5 eqid ⊢ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) }
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) ) → 𝐺 dom DProd 𝑆 )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) ) → dom 𝑆 = 𝐼 )
8 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) ) → 𝑋 ∈ 𝐼 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) ) → 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) )
10 eqid ⊢ ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝑥 , ( 0g ‘ 𝐺 ) ) ) = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝑥 , ( 0g ‘ 𝐺 ) ) )
11 4 5 6 7 8 9 10 dprdfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) ) → ( ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝑥 , ( 0g ‘ 𝐺 ) ) ) ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝑥 , ( 0g ‘ 𝐺 ) ) ) ) = 𝑥 ) )
12 11 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) ) → ( 𝐺 Σg ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝑥 , ( 0g ‘ 𝐺 ) ) ) ) = 𝑥 )
13 11 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) ) → ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝑥 , ( 0g ‘ 𝐺 ) ) ) ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
14 4 5 6 7 13 eldprdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) ) → ( 𝐺 Σg ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝑥 , ( 0g ‘ 𝐺 ) ) ) ) ∈ ( 𝐺 DProd 𝑆 ) )
15 12 14 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) ) → 𝑥 ∈ ( 𝐺 DProd 𝑆 ) )
16 15 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑆 ‘ 𝑋 ) → 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ) )
17 16 ssrdv ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝐺 DProd 𝑆 ) )