lmat22e12

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

Metamath Proof Explorer

Theorem lmat22e12

Proof