lmat22e22

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

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

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		1nn0	⊢ 1 ∈ ℕ₀
15	6	nnrei	⊢ 2 ∈ ℝ
16	15	leidi	⊢ 2 ≤ 2
17		1p1e2	⊢ ( 1 + 1 ) = 2
18		s2cli	⊢ ⟨“ 𝐶 𝐷 ”⟩ ∈ Word V
19		s2fv1	⊢ ( ⟨“ 𝐶 𝐷 ”⟩ ∈ Word V → ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 1 ) = ⟨“ 𝐶 𝐷 ”⟩ )
20	18 19	ax-mp	⊢ ( ⟨“ ⟨“ 𝐴 𝐵 ”⟩ ⟨“ 𝐶 𝐷 ”⟩ ”⟩ ‘ 1 ) = ⟨“ 𝐶 𝐷 ”⟩
21		s2fv1	⊢ ( 𝐷 ∈ 𝑉 → ( ⟨“ 𝐶 𝐷 ”⟩ ‘ 1 ) = 𝐷 )
22	5 21	syl	⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 ”⟩ ‘ 1 ) = 𝐷 )
23	1 7 10 12 13 14 14 16 16 17 17 20 22	lmatfvlem	⊢ ( 𝜑 → ( 2 𝑀 2 ) = 𝐷 )

Metamath Proof Explorer

Theorem lmat22e22

Proof