Theorem lmat22lem

Description: Lemma for lmat22e11 and co. (Contributed by Thierry Arnoux, 28-Aug-2020)

	Ref	Expression
Hypotheses	lmat22.m	⊢ 𝑀 = ( litMat ‘ ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ )
	lmat22.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	lmat22.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	lmat22.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	lmat22.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion	lmat22lem	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 2 ) ) → ( ♯ ‘ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) ) = 2 )

Proof

Step	Hyp	Ref	Expression
1		lmat22.m	⊢ 𝑀 = ( litMat ‘ ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ )
2		lmat22.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		lmat22.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		lmat22.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		lmat22.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → 𝑖 = 0 )
7	6	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) = ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 0 ) )
8	2 3	s2cld	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 )
9		s2fv0	⊢ ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 0 ) = ⟨“ 𝐴 𝐵 ”⟩ )
10	8 9	syl	⊢ ( 𝜑 → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 0 ) = ⟨“ 𝐴 𝐵 ”⟩ )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 0 ) = ⟨“ 𝐴 𝐵 ”⟩ )
12	7 11	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) = ⟨“ 𝐴 𝐵 ”⟩ )
13	12	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ♯ ‘ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) ) = ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) )
14		s2len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 2
15	13 14	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ♯ ‘ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) ) = 2 )
16	15	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 2 ) ) ∧ 𝑖 = 0 ) → ( ♯ ‘ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) ) = 2 )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → 𝑖 = 1 )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) = ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 1 ) )
19	4 5	s2cld	⊢ ( 𝜑 → ⟨“ 𝐶 𝐷 ”⟩ ∈ Word 𝑉 )
20		s2fv1	⊢ ( ⟨“ 𝐶 𝐷 ”⟩ ∈ Word 𝑉 → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 1 ) = ⟨“ 𝐶 𝐷 ”⟩ )
21	19 20	syl	⊢ ( 𝜑 → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 1 ) = ⟨“ 𝐶 𝐷 ”⟩ )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 1 ) = ⟨“ 𝐶 𝐷 ”⟩ )
23	18 22	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) = ⟨“ 𝐶 𝐷 ”⟩ )
24	23	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ♯ ‘ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) ) = ( ♯ ‘ ⟨“ 𝐶 𝐷 ”⟩ ) )
25		s2len	⊢ ( ♯ ‘ ⟨“ 𝐶 𝐷 ”⟩ ) = 2
26	24 25	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑖 = 1 ) → ( ♯ ‘ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) ) = 2 )
27	26	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 2 ) ) ∧ 𝑖 = 1 ) → ( ♯ ‘ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) ) = 2 )
28		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
29	28	eleq2i	⊢ ( 𝑖 ∈ ( 0 ..^ 2 ) ↔ 𝑖 ∈ { 0 , 1 } )
30		vex	⊢ 𝑖 ∈ V
31	30	elpr	⊢ ( 𝑖 ∈ { 0 , 1 } ↔ ( 𝑖 = 0 ∨ 𝑖 = 1 ) )
32	29 31	bitri	⊢ ( 𝑖 ∈ ( 0 ..^ 2 ) ↔ ( 𝑖 = 0 ∨ 𝑖 = 1 ) )
33	32	bilani	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 2 ) ) → ( 𝑖 = 0 ∨ 𝑖 = 1 ) )
34	16 27 33	mpjaodan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 2 ) ) → ( ♯ ‘ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) ) = 2 )