Metamath Proof Explorer

Theorem stoweidlem6

Description: Lemma for stoweid : two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem6.1 ⊢ Ⅎ 𝑡 𝑓 = 𝐹
stoweidlem6.2 ⊢ Ⅎ 𝑡 𝑔 = 𝐺
stoweidlem6.3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
Assertion stoweidlem6 ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 stoweidlem6.1 ⊢ Ⅎ 𝑡 𝑓 = 𝐹
2 stoweidlem6.2 ⊢ Ⅎ 𝑡 𝑔 = 𝐺
3 stoweidlem6.3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
4 simp3 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 ∈ 𝐴 )
5 eleq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴 ) )
6 5 3anbi3d ⊢ ( 𝑔 = 𝐺 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ) )
7 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑡 ) )
8 7 oveq2d ⊢ ( 𝑔 = 𝐺 → ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
9 8 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
10 2 9 mpteq2da ⊢ ( 𝑔 = 𝐺 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) )
11 10 eleq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
12 6 11 imbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
13 simp2 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → 𝐹 ∈ 𝐴 )
14 eleq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ 𝐴 ↔ 𝐹 ∈ 𝐴 ) )
15 14 3anbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ) )
16 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
17 16 oveq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
18 17 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
19 1 18 mpteq2da ⊢ ( 𝑓 = 𝐹 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
20 19 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
21 15 20 imbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
22 21 3 vtoclg ⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
23 13 22 mpcom ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
24 12 23 vtoclg ⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
25 4 24 mpcom ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )