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

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 = ( 0g ‘ 𝐺 )
Assertion dprd0 ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) )

Proof

Step Hyp Ref Expression
1 dprd0.0 ⊢ 0 = ( 0g ‘ 𝐺 )
2 0ex ⊢ ∅ ∈ V
3 1 dprdz ⊢ ( ( 𝐺 ∈ Grp ∧ ∅ ∈ V ) → ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) )
4 2 3 mpan2 ⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) )
5 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ { 0 } ) = ∅
6 5 breq2i ⊢ ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ↔ 𝐺 dom DProd ∅ )
7 5 oveq2i ⊢ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = ( 𝐺 DProd ∅ )
8 7 eqeq1i ⊢ ( ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ↔ ( 𝐺 DProd ∅ ) = { 0 } )
9 6 8 anbi12i ⊢ ( ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) ↔ ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) )
10 4 9 sylib ⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) )