Theorem lmat22e22

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

	Ref	Expression
Hypotheses	lmat22.m	|- M = ( litMat ` <" <" A B "> <" C D "> "> )
	lmat22.a	|- ( ph -> A e. V )
	lmat22.b	|- ( ph -> B e. V )
	lmat22.c	|- ( ph -> C e. V )
	lmat22.d	|- ( ph -> D e. V )
Assertion	lmat22e22	|- ( ph -> ( 2 M 2 ) = D )

Proof

Step	Hyp	Ref	Expression
1		lmat22.m	|- M = ( litMat ` <" <" A B "> <" C D "> "> )
2		lmat22.a	|- ( ph -> A e. V )
3		lmat22.b	|- ( ph -> B e. V )
4		lmat22.c	|- ( ph -> C e. V )
5		lmat22.d	|- ( ph -> D e. V )
6		2nn	|- 2 e. NN
7	6	a1i	|- ( ph -> 2 e. NN )
8	2 3	s2cld	|- ( ph -> <" A B "> e. Word V )
9	4 5	s2cld	|- ( ph -> <" C D "> e. Word V )
10	8 9	s2cld	|- ( ph -> <" <" A B "> <" C D "> "> e. Word Word V )
11		s2len	|- ( # ` <" <" A B "> <" C D "> "> ) = 2
12	11	a1i	|- ( ph -> ( # ` <" <" A B "> <" C D "> "> ) = 2 )
13	1 2 3 4 5	lmat22lem	|- ( ( ph /\ i e. ( 0 ..^ 2 ) ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 )
14		1nn0	|- 1 e. NN0
15	6	nnrei	|- 2 e. RR
16	15	leidi	|- 2 <_ 2
17		1p1e2	|- ( 1 + 1 ) = 2
18		s2cli	|- <" C D "> e. Word _V
19		s2fv1	|- ( <" C D "> e. Word _V -> ( <" <" A B "> <" C D "> "> ` 1 ) = <" C D "> )
20	18 19	ax-mp	|- ( <" <" A B "> <" C D "> "> ` 1 ) = <" C D ">
21		s2fv1	|- ( D e. V -> ( <" C D "> ` 1 ) = D )
22	5 21	syl	|- ( ph -> ( <" C D "> ` 1 ) = D )
23	1 7 10 12 13 14 14 16 16 17 17 20 22	lmatfvlem	|- ( ph -> ( 2 M 2 ) = D )