dih1dimatlem0

	Ref	Expression
Hypotheses	dih1dimat.h	$⊢ H = LHyp (K)$
	dih1dimat.u	$⊢ U = DVecH (K) (W)$
	dih1dimat.i	$⊢ I = DIsoH (K) (W)$
	dih1dimat.a	$⊢ A = LSAtoms (U)$
	dih1dimat.b	$⊢ B = {Base}_{K}$
	dih1dimat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dih1dimat.c	$⊢ C = Atoms (K)$
	dih1dimat.p	$⊢ P = oc (K) (W)$
	dih1dimat.t	$⊢ T = LTrn (K) (W)$
	dih1dimat.r	$⊢ R = trL (K) (W)$
	dih1dimat.e	$⊢ E = TEndo (K) (W)$
	dih1dimat.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	dih1dimat.d	$⊢ F = Scalar (U)$
	dih1dimat.j	$⊢ J = {inv}_{r} (F)$
	dih1dimat.v	$⊢ V = {Base}_{U}$
	dih1dimat.m	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	dih1dimat.s	$⊢ S = LSubSp (U)$
	dih1dimat.n	$⊢ N = LSpan (U)$
	dih1dimat.z	$⊢ \underset{˙}{0} = 0_{U}$
	dih1dimat.g	$⊢ G = (ι h \in T \| h (P) = J (s) (f) (P))$
Assertion	dih1dimatlem0	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to ((i = p (G) \land p \in E) \leftrightarrow ((i \in T \land p \in E) \land \exists t \in E (i = t (f) \land p = t \circ s)))$

Proof

Step	Hyp	Ref	Expression
1		dih1dimat.h	$⊢ H = LHyp (K)$
2		dih1dimat.u	$⊢ U = DVecH (K) (W)$
3		dih1dimat.i	$⊢ I = DIsoH (K) (W)$
4		dih1dimat.a	$⊢ A = LSAtoms (U)$
5		dih1dimat.b	$⊢ B = {Base}_{K}$
6		dih1dimat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
7		dih1dimat.c	$⊢ C = Atoms (K)$
8		dih1dimat.p	$⊢ P = oc (K) (W)$
9		dih1dimat.t	$⊢ T = LTrn (K) (W)$
10		dih1dimat.r	$⊢ R = trL (K) (W)$
11		dih1dimat.e	$⊢ E = TEndo (K) (W)$
12		dih1dimat.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
13		dih1dimat.d	$⊢ F = Scalar (U)$
14		dih1dimat.j	$⊢ J = {inv}_{r} (F)$
15		dih1dimat.v	$⊢ V = {Base}_{U}$
16		dih1dimat.m	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
17		dih1dimat.s	$⊢ S = LSubSp (U)$
18		dih1dimat.n	$⊢ N = LSpan (U)$
19		dih1dimat.z	$⊢ \underset{˙}{0} = 0_{U}$
20		dih1dimat.g	$⊢ G = (ι h \in T \| h (P) = J (s) (f) (P))$
21		simprl	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to i = p (G)$
22		simpl1	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to (K \in HL \land W \in H)$
23		simprr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to p \in E$
24	6 7 1 8	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in C \land \neg P \underset{˙}{\leq} W)$
25	22 24	syl	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to (P \in C \land \neg P \underset{˙}{\leq} W)$
26		simpl2r	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to s \in E$
27		simpl3	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to s \neq O$
28	5 1 9 11 12 2 13 14	tendoinvcl	$⊢ ((K \in HL \land W \in H) \land s \in E \land s \neq O) \to (J (s) \in E \land J (s) \neq O)$
29	28	simpld	$⊢ ((K \in HL \land W \in H) \land s \in E \land s \neq O) \to J (s) \in E$
30	22 26 27 29	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to J (s) \in E$
31		simpl2l	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to f \in T$
32	1 9 11	tendocl	$⊢ ((K \in HL \land W \in H) \land J (s) \in E \land f \in T) \to J (s) (f) \in T$
33	22 30 31 32	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to J (s) (f) \in T$
34	6 7 1 9	ltrnel	$⊢ ((K \in HL \land W \in H) \land J (s) (f) \in T \land (P \in C \land \neg P \underset{˙}{\leq} W)) \to (J (s) (f) (P) \in C \land \neg J (s) (f) (P) \underset{˙}{\leq} W)$
35	22 33 25 34	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to (J (s) (f) (P) \in C \land \neg J (s) (f) (P) \underset{˙}{\leq} W)$
36	6 7 1 9 20	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in C \land \neg P \underset{˙}{\leq} W) \land (J (s) (f) (P) \in C \land \neg J (s) (f) (P) \underset{˙}{\leq} W)) \to G \in T$
37	22 25 35 36	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to G \in T$
38	1 9 11	tendocl	$⊢ ((K \in HL \land W \in H) \land p \in E \land G \in T) \to p (G) \in T$
39	22 23 37 38	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to p (G) \in T$
40	21 39	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to i \in T$
41	1 11	tendococl	$⊢ ((K \in HL \land W \in H) \land p \in E \land J (s) \in E) \to p \circ J (s) \in E$
42	22 23 30 41	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to p \circ J (s) \in E$
43		simp1	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to (K \in HL \land W \in H)$
44	24	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to (P \in C \land \neg P \underset{˙}{\leq} W)$
45	29	3adant2l	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to J (s) \in E$
46		simp2l	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to f \in T$
47	43 45 46 32	syl3anc	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to J (s) (f) \in T$
48	43 47 44 34	syl3anc	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to (J (s) (f) (P) \in C \land \neg J (s) (f) (P) \underset{˙}{\leq} W)$
49	43 44 48 36	syl3anc	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to G \in T$
50	6 7 1 9 20	ltrniotaval	$⊢ ((K \in HL \land W \in H) \land (P \in C \land \neg P \underset{˙}{\leq} W) \land (J (s) (f) (P) \in C \land \neg J (s) (f) (P) \underset{˙}{\leq} W)) \to G (P) = J (s) (f) (P)$
51	43 44 48 50	syl3anc	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to G (P) = J (s) (f) (P)$
52	6 7 1 9	cdlemd	$⊢ (((K \in HL \land W \in H) \land G \in T \land J (s) (f) \in T) \land (P \in C \land \neg P \underset{˙}{\leq} W) \land G (P) = J (s) (f) (P)) \to G = J (s) (f)$
53	43 49 47 44 51 52	syl311anc	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to G = J (s) (f)$
54	53	adantr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to G = J (s) (f)$
55	54	fveq2d	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to p (G) = p (J (s) (f))$
56	1 9 11	tendocoval	$⊢ ((K \in HL \land W \in H) \land (p \in E \land J (s) \in E) \land f \in T) \to (p \circ J (s)) (f) = p (J (s) (f))$
57	22 23 30 31 56	syl121anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to (p \circ J (s)) (f) = p (J (s) (f))$
58	55 21 57	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to i = (p \circ J (s)) (f)$
59		coass	$⊢ (p \circ J (s)) \circ s = p \circ (J (s) \circ s)$
60	5 1 9 11 12 2 13 14	tendolinv	$⊢ ((K \in HL \land W \in H) \land s \in E \land s \neq O) \to J (s) \circ s = {I ↾}_{T}$
61	22 26 27 60	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to J (s) \circ s = {I ↾}_{T}$
62	61	coeq2d	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to p \circ (J (s) \circ s) = p \circ ({I ↾}_{T})$
63	1 9 11	tendo1mulr	$⊢ ((K \in HL \land W \in H) \land p \in E) \to p \circ ({I ↾}_{T}) = p$
64	22 23 63	syl2anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to p \circ ({I ↾}_{T}) = p$
65	62 64	eqtrd	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to p \circ (J (s) \circ s) = p$
66	59 65	eqtr2id	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to p = (p \circ J (s)) \circ s$
67		fveq1	$⊢ t = p \circ J (s) \to t (f) = (p \circ J (s)) (f)$
68	67	eqeq2d	$⊢ t = p \circ J (s) \to (i = t (f) \leftrightarrow i = (p \circ J (s)) (f))$
69		coeq1	$⊢ t = p \circ J (s) \to t \circ s = (p \circ J (s)) \circ s$
70	69	eqeq2d	$⊢ t = p \circ J (s) \to (p = t \circ s \leftrightarrow p = (p \circ J (s)) \circ s)$
71	68 70	anbi12d	$⊢ t = p \circ J (s) \to ((i = t (f) \land p = t \circ s) \leftrightarrow (i = (p \circ J (s)) (f) \land p = (p \circ J (s)) \circ s))$
72	71	rspcev	$⊢ (p \circ J (s) \in E \land (i = (p \circ J (s)) (f) \land p = (p \circ J (s)) \circ s)) \to \exists t \in E (i = t (f) \land p = t \circ s)$
73	42 58 66 72	syl12anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to \exists t \in E (i = t (f) \land p = t \circ s)$
74	40 23 73	jca31	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i = p (G) \land p \in E)) \to ((i \in T \land p \in E) \land \exists t \in E (i = t (f) \land p = t \circ s))$
75		simp3r	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to p = t \circ s$
76	75	fveq1d	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to p (J (s) (f)) = (t \circ s) (J (s) (f))$
77		simp1l1	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to (K \in HL \land W \in H)$
78		simp2	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to t \in E$
79		simpl2r	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \to s \in E$
80	79	3ad2ant1	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to s \in E$
81	1 11	tendococl	$⊢ ((K \in HL \land W \in H) \land t \in E \land s \in E) \to t \circ s \in E$
82	77 78 80 81	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to t \circ s \in E$
83		simp1l3	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to s \neq O$
84	77 80 83 29	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to J (s) \in E$
85		simpl2l	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \to f \in T$
86	85	3ad2ant1	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to f \in T$
87	1 9 11	tendocoval	$⊢ ((K \in HL \land W \in H) \land (t \circ s \in E \land J (s) \in E) \land f \in T) \to ((t \circ s) \circ J (s)) (f) = (t \circ s) (J (s) (f))$
88	77 82 84 86 87	syl121anc	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to ((t \circ s) \circ J (s)) (f) = (t \circ s) (J (s) (f))$
89		coass	$⊢ (t \circ s) \circ J (s) = t \circ (s \circ J (s))$
90	5 1 9 11 12 2 13 14	tendorinv	$⊢ ((K \in HL \land W \in H) \land s \in E \land s \neq O) \to s \circ J (s) = {I ↾}_{T}$
91	77 80 83 90	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to s \circ J (s) = {I ↾}_{T}$
92	91	coeq2d	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to t \circ (s \circ J (s)) = t \circ ({I ↾}_{T})$
93	1 9 11	tendo1mulr	$⊢ ((K \in HL \land W \in H) \land t \in E) \to t \circ ({I ↾}_{T}) = t$
94	77 78 93	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to t \circ ({I ↾}_{T}) = t$
95	92 94	eqtrd	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to t \circ (s \circ J (s)) = t$
96	89 95	syl5eq	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to (t \circ s) \circ J (s) = t$
97	96	fveq1d	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to ((t \circ s) \circ J (s)) (f) = t (f)$
98	76 88 97	3eqtr2rd	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to t (f) = p (J (s) (f))$
99		simp3l	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to i = t (f)$
100	53	adantr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \to G = J (s) (f)$
101	100	3ad2ant1	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to G = J (s) (f)$
102	101	fveq2d	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to p (G) = p (J (s) (f))$
103	98 99 102	3eqtr4d	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \land t \in E \land (i = t (f) \land p = t \circ s)) \to i = p (G)$
104	103	rexlimdv3a	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land (i \in T \land p \in E)) \to (\exists t \in E (i = t (f) \land p = t \circ s) \to i = p (G))$
105	104	impr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land ((i \in T \land p \in E) \land \exists t \in E (i = t (f) \land p = t \circ s))) \to i = p (G)$
106		simprlr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land ((i \in T \land p \in E) \land \exists t \in E (i = t (f) \land p = t \circ s))) \to p \in E$
107	105 106	jca	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \land ((i \in T \land p \in E) \land \exists t \in E (i = t (f) \land p = t \circ s))) \to (i = p (G) \land p \in E)$
108	74 107	impbida	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to ((i = p (G) \land p \in E) \leftrightarrow ((i \in T \land p \in E) \land \exists t \in E (i = t (f) \land p = t \circ s)))$

Metamath Proof Explorer

Theorem dih1dimatlem0

Proof