Metamath Proof Explorer

Theorem dprd0

Description: The empty family is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypothesis dprd0.0 ⊢ 0 ˙ = 0 G
Assertion dprd0 ⊢ G ∈ Grp → G dom ⁡ DProd ∅ ∧ G DProd ∅ = 0 ˙

Proof

Step Hyp Ref Expression
1 dprd0.0 ⊢ 0 ˙ = 0 G
2 0ex ⊢ ∅ ∈ V
3 1 dprdz ⊢ G ∈ Grp ∧ ∅ ∈ V → G dom ⁡ DProd x ∈ ∅ ⟼ 0 ˙ ∧ G DProd x ∈ ∅ ⟼ 0 ˙ = 0 ˙
4 2 3 mpan2 ⊢ G ∈ Grp → G dom ⁡ DProd x ∈ ∅ ⟼ 0 ˙ ∧ G DProd x ∈ ∅ ⟼ 0 ˙ = 0 ˙
5 mpt0 ⊢ x ∈ ∅ ⟼ 0 ˙ = ∅
6 5 breq2i ⊢ G dom ⁡ DProd x ∈ ∅ ⟼ 0 ˙ ↔ G dom ⁡ DProd ∅
7 5 oveq2i ⊢ G DProd x ∈ ∅ ⟼ 0 ˙ = G DProd ∅
8 7 eqeq1i ⊢ G DProd x ∈ ∅ ⟼ 0 ˙ = 0 ˙ ↔ G DProd ∅ = 0 ˙
9 6 8 anbi12i ⊢ G dom ⁡ DProd x ∈ ∅ ⟼ 0 ˙ ∧ G DProd x ∈ ∅ ⟼ 0 ˙ = 0 ˙ ↔ G dom ⁡ DProd ∅ ∧ G DProd ∅ = 0 ˙
10 4 9 sylib ⊢ G ∈ Grp → G dom ⁡ DProd ∅ ∧ G DProd ∅ = 0 ˙