Metamath Proof Explorer


Theorem 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 ∈ ℕ0
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 ) = 𝐷 )