Metamath Proof Explorer


Theorem lmat22e12

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

Ref Expression
Hypotheses lmat22.m M = litMat ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩
lmat22.a φ A V
lmat22.b φ B V
lmat22.c φ C V
lmat22.d φ D V
Assertion lmat22e12 φ 1 M 2 = B

Proof

Step Hyp Ref Expression
1 lmat22.m M = litMat ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩
2 lmat22.a φ A V
3 lmat22.b φ B V
4 lmat22.c φ C V
5 lmat22.d φ D V
6 2nn 2
7 6 a1i φ 2
8 2 3 s2cld φ ⟨“ AB ”⟩ Word V
9 4 5 s2cld φ ⟨“ CD ”⟩ Word V
10 8 9 s2cld φ ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ Word Word V
11 s2len ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ = 2
12 11 a1i φ ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ = 2
13 1 2 3 4 5 lmat22lem φ i 0 ..^ 2 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = 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 ⟨“ AB ”⟩ Word V
22 s2fv0 ⟨“ AB ”⟩ Word V ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 0 = ⟨“ AB ”⟩
23 21 22 ax-mp ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 0 = ⟨“ AB ”⟩
24 s2fv1 B V ⟨“ AB ”⟩ 1 = B
25 3 24 syl φ ⟨“ AB ”⟩ 1 = B
26 1 7 10 12 13 14 15 16 18 19 20 23 25 lmatfvlem φ 1 M 2 = B