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

Metamath Proof Explorer

Theorem ofc12

Description: Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses ofc12.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ofc12.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
ofc12.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
Assertion ofc12 ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 ( 𝐴 × { 𝐶 } ) ) = ( 𝐴 × { ( 𝐵 𝑅 𝐶 ) } ) )

Proof

Step Hyp Ref Expression
1 ofc12.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 ofc12.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 ofc12.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
4 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 )
6 fconstmpt ⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7 6 a1i ⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
8 fconstmpt ⊢ ( 𝐴 × { 𝐶 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
9 8 a1i ⊢ ( 𝜑 → ( 𝐴 × { 𝐶 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
10 1 4 5 7 9 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 ( 𝐴 × { 𝐶 } ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
11 fconstmpt ⊢ ( 𝐴 × { ( 𝐵 𝑅 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) )
12 10 11 eqtr4di ⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 ( 𝐴 × { 𝐶 } ) ) = ( 𝐴 × { ( 𝐵 𝑅 𝐶 ) } ) )