Theorem lmat22e11

Description: Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020)

	Ref	Expression
Hypotheses	lmat22.m	⊢ 𝑀 = ( litMat ‘ ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ )
	lmat22.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	lmat22.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	lmat22.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	lmat22.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion	lmat22e11	⊢ ( 𝜑 → ( 1 𝑀 1 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		lmat22.m	⊢ 𝑀 = ( litMat ‘ ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ )
2		lmat22.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		lmat22.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		lmat22.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		lmat22.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
6		2nn	⊢ 2 ∈ ℕ
7	6	a1i	⊢ ( 𝜑 → 2 ∈ ℕ )
8	2 3	s2cld	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 )
9	4 5	s2cld	⊢ ( 𝜑 → ⟨“ 𝐶 𝐷 ”⟩ ∈ Word 𝑉 )
10	8 9	s2cld	⊢ ( 𝜑 → ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ∈ Word Word 𝑉 )
11		s2len	⊢ ( ♯ ‘ ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ) = 2
12	11	a1i	⊢ ( 𝜑 → ( ♯ ‘ ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ) = 2 )
13	1 2 3 4 5	lmat22lem	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 2 ) ) → ( ♯ ‘ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 𝑖 ) ) = 2 )
14		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
15		eluzfz1	⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 2 ) )
16	14 15	ax-mp	⊢ 1 ∈ ( 1 ... 2 )
17	16	a1i	⊢ ( 𝜑 → 1 ∈ ( 1 ... 2 ) )
18	1 7 10 12 13 17 17	lmatfval	⊢ ( 𝜑 → ( 1 𝑀 1 ) = ( ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ ( 1 − 1 ) ) ‘ ( 1 − 1 ) ) )
19		1m1e0	⊢ ( 1 − 1 ) = 0
20	19	fveq2i	⊢ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ ( 1 − 1 ) ) = ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 0 )
21		s2fv0	⊢ ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 0 ) = ⟨“ 𝐴 𝐵 ”⟩ )
22	8 21	syl	⊢ ( 𝜑 → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 0 ) = ⟨“ 𝐴 𝐵 ”⟩ )
23	20 22	syl5eq	⊢ ( 𝜑 → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ ( 1 − 1 ) ) = ⟨“ 𝐴 𝐵 ”⟩ )
24	19	a1i	⊢ ( 𝜑 → ( 1 − 1 ) = 0 )
25	23 24	fveq12d	⊢ ( 𝜑 → ( ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ ( 1 − 1 ) ) ‘ ( 1 − 1 ) ) = ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) )
26		s2fv0	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) = 𝐴 )
27	2 26	syl	⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) = 𝐴 )
28	18 25 27	3eqtrd	⊢ ( 𝜑 → ( 1 𝑀 1 ) = 𝐴 )