Metamath Proof Explorer


Theorem 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 ∈ ℕ0
15 1nn0 1 ∈ ℕ0
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 ) = 𝐵 )