Theorem lpadlem3

Description: Lemma for lpadlen1 . (Contributed by Thierry Arnoux, 7-Aug-2023)

	Ref	Expression
Hypotheses	lpadlen.1	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
	lpadlen.2	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
	lpadlen.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
	lpadlen1.1	⊢ ( 𝜑 → 𝐿 ≤ ( ♯ ‘ 𝑊 ) )
Assertion	lpadlem3	⊢ ( 𝜑 → ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		lpadlen.1	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
2		lpadlen.2	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
3		lpadlen.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
4		lpadlen1.1	⊢ ( 𝜑 → 𝐿 ≤ ( ♯ ‘ 𝑊 ) )
5		lencl	⊢ ( 𝑊 ∈ Word 𝑆 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
6	2 5	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
7	6	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
8	1	nn0zd	⊢ ( 𝜑 → 𝐿 ∈ ℤ )
9		fzo0n	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) ↔ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) = ∅ ) )
10	9	biimpa	⊢ ( ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) = ∅ )
11	7 8 4 10	syl21anc	⊢ ( 𝜑 → ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) = ∅ )
12	11	xpeq1d	⊢ ( 𝜑 → ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) = ( ∅ × { 𝐶 } ) )
13		0xp	⊢ ( ∅ × { 𝐶 } ) = ∅
14	12 13	eqtrdi	⊢ ( 𝜑 → ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) = ∅ )