lmat22lem

	Ref	Expression
Hypotheses	lmat22.m	$⊢ M = litMat (⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩)$
	lmat22.a	$⊢ φ \to A \in V$
	lmat22.b	$⊢ φ \to B \in V$
	lmat22.c	$⊢ φ \to C \in V$
	lmat22.d	$⊢ φ \to D \in V$
Assertion	lmat22lem	$⊢ (φ \land i \in (0 ..^2)) \to \|⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i)\| = 2$

Proof

Step	Hyp	Ref	Expression
1		lmat22.m	$⊢ M = litMat (⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩)$
2		lmat22.a	$⊢ φ \to A \in V$
3		lmat22.b	$⊢ φ \to B \in V$
4		lmat22.c	$⊢ φ \to C \in V$
5		lmat22.d	$⊢ φ \to D \in V$
6		simpr	$⊢ (φ \land i = 0) \to i = 0$
7	6	fveq2d	$⊢ (φ \land i = 0) \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i) = ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (0)$
8	2 3	s2cld	$⊢ φ \to ⟨“ A B ”⟩ \in Word V$
9		s2fv0	$⊢ ⟨“ A B ”⟩ \in Word V \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (0) = ⟨“ A B ”⟩$
10	8 9	syl	$⊢ φ \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (0) = ⟨“ A B ”⟩$
11	10	adantr	$⊢ (φ \land i = 0) \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (0) = ⟨“ A B ”⟩$
12	7 11	eqtrd	$⊢ (φ \land i = 0) \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i) = ⟨“ A B ”⟩$
13	12	fveq2d	$⊢ (φ \land i = 0) \to \|⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i)\| = \|⟨“ A B ”⟩\|$
14		s2len	$⊢ \|⟨“ A B ”⟩\| = 2$
15	13 14	eqtrdi	$⊢ (φ \land i = 0) \to \|⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i)\| = 2$
16	15	adantlr	$⊢ ((φ \land i \in (0 ..^2)) \land i = 0) \to \|⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i)\| = 2$
17		simpr	$⊢ (φ \land i = 1) \to i = 1$
18	17	fveq2d	$⊢ (φ \land i = 1) \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i) = ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (1)$
19	4 5	s2cld	$⊢ φ \to ⟨“ C D ”⟩ \in Word V$
20		s2fv1	$⊢ ⟨“ C D ”⟩ \in Word V \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (1) = ⟨“ C D ”⟩$
21	19 20	syl	$⊢ φ \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (1) = ⟨“ C D ”⟩$
22	21	adantr	$⊢ (φ \land i = 1) \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (1) = ⟨“ C D ”⟩$
23	18 22	eqtrd	$⊢ (φ \land i = 1) \to ⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i) = ⟨“ C D ”⟩$
24	23	fveq2d	$⊢ (φ \land i = 1) \to \|⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i)\| = \|⟨“ C D ”⟩\|$
25		s2len	$⊢ \|⟨“ C D ”⟩\| = 2$
26	24 25	eqtrdi	$⊢ (φ \land i = 1) \to \|⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i)\| = 2$
27	26	adantlr	$⊢ ((φ \land i \in (0 ..^2)) \land i = 1) \to \|⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i)\| = 2$
28		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
29	28	eleq2i	$⊢ i \in (0 ..^2) \leftrightarrow i \in \{0, 1\}$
30		vex	$⊢ i \in V$
31	30	elpr	$⊢ i \in \{0, 1\} \leftrightarrow (i = 0 \lor i = 1)$
32	29 31	bitri	$⊢ i \in (0 ..^2) \leftrightarrow (i = 0 \lor i = 1)$
33	32	biimpi	$⊢ i \in (0 ..^2) \to (i = 0 \lor i = 1)$
34	33	adantl	$⊢ (φ \land i \in (0 ..^2)) \to (i = 0 \lor i = 1)$
35	16 27 34	mpjaodan	$⊢ (φ \land i \in (0 ..^2)) \to \|⟨“ ⟨“ A B ”⟩ ⟨“ C D ”⟩ ”⟩ (i)\| = 2$

Metamath Proof Explorer

Theorem lmat22lem

Proof