Metamath Proof Explorer

Theorem dihordlem6

Description: Part of proof of Lemma N of Crawley p. 122 line 35. (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	dihordlem6	$⊢ ((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)) \to ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ = ⟨s (G) \circ g, 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		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)) \to (K \in HL \land W \in H)$
13		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)) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
14		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)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
15		simp3	$⊢ ((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)) \to (s \in E \land g \in T)$
16	1 2 3 4 5 6 7 8 9 10 11	cdlemn6	$⊢ ((K \in HL \land W \in H) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (s \in E \land g \in T)) \to ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ = ⟨s (G) \circ g, s⟩$
17	12 13 14 15 16	syl121anc	$⊢ ((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)) \to ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ = ⟨s (G) \circ g, s⟩$