Metamath Proof Explorer


Theorem lmat22lem

Description: Lemma for lmat22e11 and co. (Contributed by Thierry Arnoux, 28-Aug-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 lmat22lem φ i 0 ..^ 2 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = 2

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 simpr φ i = 0 i = 0
7 6 fveq2d φ i = 0 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 0
8 2 3 s2cld φ ⟨“ AB ”⟩ Word V
9 s2fv0 ⟨“ AB ”⟩ Word V ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 0 = ⟨“ AB ”⟩
10 8 9 syl φ ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 0 = ⟨“ AB ”⟩
11 10 adantr φ i = 0 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 0 = ⟨“ AB ”⟩
12 7 11 eqtrd φ i = 0 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = ⟨“ AB ”⟩
13 12 fveq2d φ i = 0 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = ⟨“ AB ”⟩
14 s2len ⟨“ AB ”⟩ = 2
15 13 14 syl6eq φ i = 0 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = 2
16 15 adantlr φ i 0 ..^ 2 i = 0 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = 2
17 simpr φ i = 1 i = 1
18 17 fveq2d φ i = 1 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 1
19 4 5 s2cld φ ⟨“ CD ”⟩ Word V
20 s2fv1 ⟨“ CD ”⟩ Word V ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 1 = ⟨“ CD ”⟩
21 19 20 syl φ ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 1 = ⟨“ CD ”⟩
22 21 adantr φ i = 1 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ 1 = ⟨“ CD ”⟩
23 18 22 eqtrd φ i = 1 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = ⟨“ CD ”⟩
24 23 fveq2d φ i = 1 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = ⟨“ CD ”⟩
25 s2len ⟨“ CD ”⟩ = 2
26 24 25 syl6eq φ i = 1 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = 2
27 26 adantlr φ i 0 ..^ 2 i = 1 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = 2
28 fzo0to2pr 0 ..^ 2 = 0 1
29 28 eleq2i i 0 ..^ 2 i 0 1
30 vex i V
31 30 elpr i 0 1 i = 0 i = 1
32 29 31 bitri i 0 ..^ 2 i = 0 i = 1
33 32 biimpi i 0 ..^ 2 i = 0 i = 1
34 33 adantl φ i 0 ..^ 2 i = 0 i = 1
35 16 27 34 mpjaodan φ i 0 ..^ 2 ⟨“ ⟨“ AB ”⟩ ⟨“ CD ”⟩ ”⟩ i = 2