cdlemn8

Description: Part of proof of Lemma N of Crawley p. 121 line 36. (Contributed by NM, 26-Feb-2014)

	Ref	Expression
Hypotheses	cdlemn8.b	$⊢ B = {Base}_{K}$
	cdlemn8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemn8.a	$⊢ A = Atoms (K)$
	cdlemn8.h	$⊢ H = LHyp (K)$
	cdlemn8.p	$⊢ P = oc (K) (W)$
	cdlemn8.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	cdlemn8.t	$⊢ T = LTrn (K) (W)$
	cdlemn8.e	$⊢ E = TEndo (K) (W)$
	cdlemn8.u	$⊢ U = DVecH (K) (W)$
	cdlemn8.s	$⊢ \underset{˙}{+} = +_{U}$
	cdlemn8.f	$⊢ F = (ι h \in T \| h (P) = Q)$
	cdlemn8.g	$⊢ G = (ι h \in T \| h (P) = R)$
Assertion	cdlemn8	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g = G \circ F^{-1}$

Proof

Step	Hyp	Ref	Expression
1		cdlemn8.b	$⊢ B = {Base}_{K}$
2		cdlemn8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemn8.a	$⊢ A = Atoms (K)$
4		cdlemn8.h	$⊢ H = LHyp (K)$
5		cdlemn8.p	$⊢ P = oc (K) (W)$
6		cdlemn8.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
7		cdlemn8.t	$⊢ T = LTrn (K) (W)$
8		cdlemn8.e	$⊢ E = TEndo (K) (W)$
9		cdlemn8.u	$⊢ U = DVecH (K) (W)$
10		cdlemn8.s	$⊢ \underset{˙}{+} = +_{U}$
11		cdlemn8.f	$⊢ F = (ι h \in T \| h (P) = Q)$
12		cdlemn8.g	$⊢ G = (ι h \in T \| h (P) = R)$
13		coass	$⊢ (F^{-1} \circ F) \circ g = F^{-1} \circ (F \circ g)$
14		simp1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (K \in HL \land W \in H)$
15	2 3 4 5	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
16	15	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
17		simp2l	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
18	2 3 4 7 11	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F \in T$
19	14 16 17 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to F \in T$
20	1 4 7	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
21	14 19 20	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to F : B \underset{1-1 onto}{⟶} B$
22		f1ococnv1	$⊢ F : B \underset{1-1 onto}{⟶} B \to F^{-1} \circ F = {I ↾}_{B}$
23	21 22	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to F^{-1} \circ F = {I ↾}_{B}$
24	23	coeq1d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (F^{-1} \circ F) \circ g = ({I ↾}_{B}) \circ g$
25		simp32	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g \in T$
26	1 4 7	ltrn1o	$⊢ ((K \in HL \land W \in H) \land g \in T) \to g : B \underset{1-1 onto}{⟶} B$
27	14 25 26	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g : B \underset{1-1 onto}{⟶} B$
28		f1of	$⊢ g : B \underset{1-1 onto}{⟶} B \to g : B ⟶ B$
29		fcoi2	$⊢ g : B ⟶ B \to ({I ↾}_{B}) \circ g = g$
30	27 28 29	3syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ({I ↾}_{B}) \circ g = g$
31	24 30	eqtr2d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g = (F^{-1} \circ F) \circ g$
32	1 2 3 4 5 6 7 8 9 10 11 12	cdlemn7	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (G = s (F) \circ g \land {I ↾}_{T} = s)$
33	32	simpld	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to G = s (F) \circ g$
34	32	simprd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to {I ↾}_{T} = s$
35	34	fveq1d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ({I ↾}_{T}) (F) = s (F)$
36		fvresi	$⊢ F \in T \to ({I ↾}_{T}) (F) = F$
37	19 36	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ({I ↾}_{T}) (F) = F$
38	35 37	eqtr3d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to s (F) = F$
39	38	coeq1d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to s (F) \circ g = F \circ g$
40	33 39	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to G = F \circ g$
41	40	coeq2d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to F^{-1} \circ G = F^{-1} \circ (F \circ g)$
42	13 31 41	3eqtr4a	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g = F^{-1} \circ G$
43	4 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
44	14 19 43	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to F^{-1} \in T$
45		simp2r	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
46	2 3 4 7 12	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to G \in T$
47	14 16 45 46	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to G \in T$
48	4 7	ltrncom	$⊢ ((K \in HL \land W \in H) \land F^{-1} \in T \land G \in T) \to F^{-1} \circ G = G \circ F^{-1}$
49	14 44 47 48	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to F^{-1} \circ G = G \circ F^{-1}$
50	42 49	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g = G \circ F^{-1}$

Metamath Proof Explorer

Theorem cdlemn8

Proof