Metamath Proof Explorer


Theorem stoweidlem12

Description: Lemma for stoweid . This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem12.1 Q=tT1PtNKN
stoweidlem12.2 φP:T
stoweidlem12.3 φN0
stoweidlem12.4 φK0
Assertion stoweidlem12 φtTQt=1PtNKN

Proof

Step Hyp Ref Expression
1 stoweidlem12.1 Q=tT1PtNKN
2 stoweidlem12.2 φP:T
3 stoweidlem12.3 φN0
4 stoweidlem12.4 φK0
5 simpr φtTtT
6 1red φtT1
7 2 ffvelrnda φtTPt
8 3 adantr φtTN0
9 7 8 reexpcld φtTPtN
10 6 9 resubcld φtT1PtN
11 4 3 jca φK0N0
12 11 adantr φtTK0N0
13 nn0expcl K0N0KN0
14 12 13 syl φtTKN0
15 10 14 reexpcld φtT1PtNKN
16 1 fvmpt2 tT1PtNKNQt=1PtNKN
17 5 15 16 syl2anc φtTQt=1PtNKN