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 ⊢ φ → G dom ⁡ DProd S
dprdub.2 ⊢ φ → dom ⁡ S = I
dprdub.3 ⊢ φ → X ∈ I
Assertion dprdub ⊢ φ → S ⁡ X ⊆ G DProd S

Proof

Step Hyp Ref Expression
1 dprdub.1 ⊢ φ → G dom ⁡ DProd S
2 dprdub.2 ⊢ φ → dom ⁡ S = I
3 dprdub.3 ⊢ φ → X ∈ I
4 eqid ⊢ 0 G = 0 G
5 eqid ⊢ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h
6 1 adantr ⊢ φ ∧ x ∈ S ⁡ X → G dom ⁡ DProd S
7 2 adantr ⊢ φ ∧ x ∈ S ⁡ X → dom ⁡ S = I
8 3 adantr ⊢ φ ∧ x ∈ S ⁡ X → X ∈ I
9 simpr ⊢ φ ∧ x ∈ S ⁡ X → x ∈ S ⁡ X
10 eqid ⊢ n ∈ I ⟼ if n = X x 0 G = n ∈ I ⟼ if n = X x 0 G
11 4 5 6 7 8 9 10 dprdfid ⊢ φ ∧ x ∈ S ⁡ X → n ∈ I ⟼ if n = X x 0 G ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ∧ ∑ G n ∈ I if n = X x 0 G = x
12 11 simprd ⊢ φ ∧ x ∈ S ⁡ X → ∑ G n ∈ I if n = X x 0 G = x
13 11 simpld ⊢ φ ∧ x ∈ S ⁡ X → n ∈ I ⟼ if n = X x 0 G ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h
14 4 5 6 7 13 eldprdi ⊢ φ ∧ x ∈ S ⁡ X → ∑ G n ∈ I if n = X x 0 G ∈ G DProd S
15 12 14 eqeltrrd ⊢ φ ∧ x ∈ S ⁡ X → x ∈ G DProd S
16 15 ex ⊢ φ → x ∈ S ⁡ X → x ∈ G DProd S
17 16 ssrdv ⊢ φ → S ⁡ X ⊆ G DProd S