dia2dimlem4

Description: Lemma for dia2dim . Show that the composition (sum) of translations (vectors) G and D equals F . Part of proof of Lemma M in Crawley p. 121 line 5. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dia2dimlem4.a	$⊢ A = Atoms (K)$
	dia2dimlem4.h	$⊢ H = LHyp (K)$
	dia2dimlem4.t	$⊢ T = LTrn (K) (W)$
	dia2dimlem4.k	$⊢ φ \to (K \in HL \land W \in H)$
	dia2dimlem4.p	$⊢ φ \to (P \in A \land \neg P \underset{˙}{\leq} W)$
	dia2dimlem4.f	$⊢ φ \to F \in T$
	dia2dimlem4.g	$⊢ φ \to G \in T$
	dia2dimlem4.gv	$⊢ φ \to G (P) = Q$
	dia2dimlem4.d	$⊢ φ \to D \in T$
	dia2dimlem4.dv	$⊢ φ \to D (Q) = F (P)$
Assertion	dia2dimlem4	$⊢ φ \to D \circ G = F$

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dia2dimlem4.a	$⊢ A = Atoms (K)$
3		dia2dimlem4.h	$⊢ H = LHyp (K)$
4		dia2dimlem4.t	$⊢ T = LTrn (K) (W)$
5		dia2dimlem4.k	$⊢ φ \to (K \in HL \land W \in H)$
6		dia2dimlem4.p	$⊢ φ \to (P \in A \land \neg P \underset{˙}{\leq} W)$
7		dia2dimlem4.f	$⊢ φ \to F \in T$
8		dia2dimlem4.g	$⊢ φ \to G \in T$
9		dia2dimlem4.gv	$⊢ φ \to G (P) = Q$
10		dia2dimlem4.d	$⊢ φ \to D \in T$
11		dia2dimlem4.dv	$⊢ φ \to D (Q) = F (P)$
12	3 4	ltrnco	$⊢ ((K \in HL \land W \in H) \land D \in T \land G \in T) \to D \circ G \in T$
13	5 10 8 12	syl3anc	$⊢ φ \to D \circ G \in T$
14	6	simpld	$⊢ φ \to P \in A$
15	1 2 3 4	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (D \in T \land G \in T) \land P \in A) \to (D \circ G) (P) = D (G (P))$
16	5 10 8 14 15	syl121anc	$⊢ φ \to (D \circ G) (P) = D (G (P))$
17	9	fveq2d	$⊢ φ \to D (G (P)) = D (Q)$
18	16 17 11	3eqtrd	$⊢ φ \to (D \circ G) (P) = F (P)$
19	1 2 3 4	cdlemd	$⊢ (((K \in HL \land W \in H) \land D \circ G \in T \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (D \circ G) (P) = F (P)) \to D \circ G = F$
20	5 13 7 6 18 19	syl311anc	$⊢ φ \to D \circ G = F$

Metamath Proof Explorer

Theorem dia2dimlem4

Proof