Metamath Proof Explorer

Theorem lpadmax

Description: Length of a left-padded word, in the general case, expressed with an if statement. (Contributed by Thierry Arnoux, 7-Aug-2023)

Ref Expression
Hypotheses lpadlen.1 
|- ( ph -> L e. NN0 )
lpadlen.2 
|- ( ph -> W e. Word S )
lpadlen.3 
|- ( ph -> C e. S )
Assertion lpadmax 
|- ( ph -> ( # ` ( ( C leftpad W ) ` L ) ) = if ( L <_ ( # ` W ) , ( # ` W ) , L ) )

Proof

Step Hyp Ref Expression
1 lpadlen.1 
 |-  ( ph -> L e. NN0 )
2 lpadlen.2 
 |-  ( ph -> W e. Word S )
3 lpadlen.3 
 |-  ( ph -> C e. S )
4 eqeq2 
 |-  ( ( # ` W ) = if ( L <_ ( # ` W ) , ( # ` W ) , L ) -> ( ( # ` ( ( C leftpad W ) ` L ) ) = ( # ` W ) <-> ( # ` ( ( C leftpad W ) ` L ) ) = if ( L <_ ( # ` W ) , ( # ` W ) , L ) ) )
5 eqeq2 
 |-  ( L = if ( L <_ ( # ` W ) , ( # ` W ) , L ) -> ( ( # ` ( ( C leftpad W ) ` L ) ) = L <-> ( # ` ( ( C leftpad W ) ` L ) ) = if ( L <_ ( # ` W ) , ( # ` W ) , L ) ) )
6 1 adantr 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> L e. NN0 )
7 2 adantr 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> W e. Word S )
8 3 adantr 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> C e. S )
9 simpr 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> L <_ ( # ` W ) )
10 6 7 8 9 lpadlen1 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> ( # ` ( ( C leftpad W ) ` L ) ) = ( # ` W ) )
11 1 adantr 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> L e. NN0 )
12 2 adantr 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> W e. Word S )
13 3 adantr 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> C e. S )
14 lencl 
 |-  ( W e. Word S -> ( # ` W ) e. NN0 )
15 2 14 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
16 15 nn0red 
 |-  ( ph -> ( # ` W ) e. RR )
17 16 adantr 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> ( # ` W ) e. RR )
18 11 nn0red 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> L e. RR )
19 1 nn0red 
 |-  ( ph -> L e. RR )
20 16 19 ltnled 
 |-  ( ph -> ( ( # ` W ) < L <-> -. L <_ ( # ` W ) ) )
21 20 biimpar 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> ( # ` W ) < L )
22 17 18 21 ltled 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> ( # ` W ) <_ L )
23 11 12 13 22 lpadlen2 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> ( # ` ( ( C leftpad W ) ` L ) ) = L )
24 4 5 10 23 ifbothda 
 |-  ( ph -> ( # ` ( ( C leftpad W ) ` L ) ) = if ( L <_ ( # ` W ) , ( # ` W ) , L ) )