dihordlem7b

Description: Part of proof of Lemma N of Crawley p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014)

	Ref	Expression
Hypotheses	dihordlem8.b	$⊢ B = {Base}_{K}$
	dihordlem8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihordlem8.a	$⊢ A = Atoms (K)$
	dihordlem8.h	$⊢ H = LHyp (K)$
	dihordlem8.p	$⊢ P = oc (K) (W)$
	dihordlem8.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	dihordlem8.t	$⊢ T = LTrn (K) (W)$
	dihordlem8.e	$⊢ E = TEndo (K) (W)$
	dihordlem8.u	$⊢ U = DVecH (K) (W)$
	dihordlem8.s	$⊢ \underset{˙}{+} = +_{U}$
	dihordlem8.g	$⊢ G = (ι h \in T \| h (P) = R)$
Assertion	dihordlem7b	$⊢ ((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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (f = g \land O = s)$

Proof

Step	Hyp	Ref	Expression
1		dihordlem8.b	$⊢ B = {Base}_{K}$
2		dihordlem8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihordlem8.a	$⊢ A = Atoms (K)$
4		dihordlem8.h	$⊢ H = LHyp (K)$
5		dihordlem8.p	$⊢ P = oc (K) (W)$
6		dihordlem8.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
7		dihordlem8.t	$⊢ T = LTrn (K) (W)$
8		dihordlem8.e	$⊢ E = TEndo (K) (W)$
9		dihordlem8.u	$⊢ U = DVecH (K) (W)$
10		dihordlem8.s	$⊢ \underset{˙}{+} = +_{U}$
11		dihordlem8.g	$⊢ G = (ι h \in T \| h (P) = R)$
12	1 2 3 4 5 6 7 8 9 10 11	dihordlem7	$⊢ ((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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (f = s (G) \circ g \land O = s)$
13	12	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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to f = s (G) \circ g$
14	12	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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to O = s$
15	14	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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to O (G) = s (G)$
16		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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (K \in HL \land W \in H)$
17	2 3 4 5	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
18	17	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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
19		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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
20	2 3 4 7 11	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$
21	16 18 19 20	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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to G \in T$
22	6 1	tendo02	$⊢ G \in T \to O (G) = {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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to O (G) = {I ↾}_{B}$
24	15 23	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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to s (G) = {I ↾}_{B}$
25	24	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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to s (G) \circ g = ({I ↾}_{B}) \circ g$
26		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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g \in T$
27	1 4 7	ltrn1o	$⊢ ((K \in HL \land W \in H) \land g \in T) \to g : B \underset{1-1 onto}{⟶} B$
28	16 26 27	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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g : B \underset{1-1 onto}{⟶} B$
29		f1of	$⊢ g : B \underset{1-1 onto}{⟶} B \to g : B ⟶ B$
30		fcoi2	$⊢ g : B ⟶ B \to ({I ↾}_{B}) \circ g = g$
31	28 29 30	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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ({I ↾}_{B}) \circ g = g$
32	13 25 31	3eqtrd	$⊢ ((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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to f = g$
33	32 14	jca	$⊢ ((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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (f = g \land O = s)$

Metamath Proof Explorer

Theorem dihordlem7b

Proof