Metamath Proof Explorer

Theorem fnlfvk3n0

Description: The value of _FL when the value of _K3 is nonzero. Part of Proposition 15.14 of TakeutiZaring p. 158. (Contributed by BTernaryTau, 17-Oct-2026)

Ref Expression
Assertion fnlfvk3n0 
|- ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _FL ` A ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) )

Proof

Step Hyp Ref Expression
1 df-fnl 
 |-  _FL = recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) )
2 1 tfr2 
 |-  ( A e. On -> ( _FL ` A ) = ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ` ( _FL |` A ) ) )
3 2 adantr 
 |-  ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _FL ` A ) = ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ` ( _FL |` A ) ) )
4 eqid 
 |-  ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) = ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) )
5 dmeq 
 |-  ( x = ( _FL |` A ) -> dom x = dom ( _FL |` A ) )
6 5 adantl 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> dom x = dom ( _FL |` A ) )
7 onss 
 |-  ( A e. On -> A C_ On )
8 1 tfr1 
 |-  _FL Fn On
9 8 fndmi 
 |-  dom _FL = On
10 9 sseq2i 
 |-  ( A C_ dom _FL <-> A C_ On )
11 ssdmres 
 |-  ( A C_ dom _FL <-> dom ( _FL |` A ) = A )
12 10 11 bitr3i 
 |-  ( A C_ On <-> dom ( _FL |` A ) = A )
13 7 12 sylib 
 |-  ( A e. On -> dom ( _FL |` A ) = A )
14 13 ad2antrr 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> dom ( _FL |` A ) = A )
15 6 14 eqtrd 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> dom x = A )
16 15 fveq2d 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( _K3 ` dom x ) = ( _K3 ` A ) )
17 simplr 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( _K3 ` A ) =/= (/) )
18 16 17 eqnetrd 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( _K3 ` dom x ) =/= (/) )
19 18 neneqd 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> -. ( _K3 ` dom x ) = (/) )
20 19 iffalsed 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) = ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) )
21 simpr 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> x = ( _FL |` A ) )
22 15 fveq2d 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( _K1 ` dom x ) = ( _K1 ` A ) )
23 21 22 fveq12d 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K1 ` dom x ) ) = ( ( _FL |` A ) ` ( _K1 ` A ) ) )
24 k39o 
 |-  ( _K3 ` A ) e. 9o
25 9on 
 |-  9o e. On
26 25 oneli 
 |-  ( ( _K3 ` A ) e. 9o -> ( _K3 ` A ) e. On )
27 24 26 ax-mp 
 |-  ( _K3 ` A ) e. On
28 on0eln0 
 |-  ( ( _K3 ` A ) e. On -> ( (/) e. ( _K3 ` A ) <-> ( _K3 ` A ) =/= (/) ) )
29 27 28 ax-mp 
 |-  ( (/) e. ( _K3 ` A ) <-> ( _K3 ` A ) =/= (/) )
30 k3n0k1lt 
 |-  ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K1 ` A ) e. A )
31 29 30 sylan2br 
 |-  ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _K1 ` A ) e. A )
32 31 fvresd 
 |-  ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ( _FL |` A ) ` ( _K1 ` A ) ) = ( _FL ` ( _K1 ` A ) ) )
33 32 adantr 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( ( _FL |` A ) ` ( _K1 ` A ) ) = ( _FL ` ( _K1 ` A ) ) )
34 23 33 eqtrd 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K1 ` dom x ) ) = ( _FL ` ( _K1 ` A ) ) )
35 15 fveq2d 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( _K2 ` dom x ) = ( _K2 ` A ) )
36 21 35 fveq12d 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K2 ` dom x ) ) = ( ( _FL |` A ) ` ( _K2 ` A ) ) )
37 k3n0k2lt 
 |-  ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K2 ` A ) e. A )
38 29 37 sylan2br 
 |-  ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _K2 ` A ) e. A )
39 38 fvresd 
 |-  ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ( _FL |` A ) ` ( _K2 ` A ) ) = ( _FL ` ( _K2 ` A ) ) )
40 39 adantr 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( ( _FL |` A ) ` ( _K2 ` A ) ) = ( _FL ` ( _K2 ` A ) ) )
41 36 40 eqtrd 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K2 ` dom x ) ) = ( _FL ` ( _K2 ` A ) ) )
42 16 34 41 oteq123d 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. = <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. )
43 42 fveq2d 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) )
44 20 43 eqtrd 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) )
45 fnfun 
 |-  ( _FL Fn On -> Fun _FL )
46 8 45 ax-mp 
 |-  Fun _FL
47 resfunexg 
 |-  ( ( Fun _FL /\ A e. On ) -> ( _FL |` A ) e. _V )
48 46 47 mpan 
 |-  ( A e. On -> ( _FL |` A ) e. _V )
49 48 adantr 
 |-  ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _FL |` A ) e. _V )
50 fvexd 
 |-  ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) e. _V )
51 4 44 49 50 fvmptd2 
 |-  ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ` ( _FL |` A ) ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) )
52 3 51 eqtrd 
 |-  ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _FL ` A ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) )