caovdilem

Description: Lemma used by real number construction. (Contributed by NM, 26-Aug-1995)

Step	Hyp	Ref	Expression
1		caovdir.1	$⊢ A \in V$
2		caovdir.2	$⊢ B \in V$
3		caovdir.3	$⊢ C \in V$
4		caovdir.com	$⊢ x G y = y G x$
5		caovdir.distr	$⊢ x G (y F z) = (x G y) F (x G z)$
6		caovdl.4	$⊢ D \in V$
7		caovdl.5	$⊢ H \in V$
8		caovdl.ass	$⊢ (x G y) G z = x G (y G z)$
9		ovex	$⊢ A G C \in V$
10		ovex	$⊢ B G D \in V$
11	9 10 7 4 5	caovdir	$⊢ ((A G C) F (B G D)) G H = ((A G C) G H) F ((B G D) G H)$
12	1 3 7 8	caovass	$⊢ (A G C) G H = A G (C G H)$
13	2 6 7 8	caovass	$⊢ (B G D) G H = B G (D G H)$
14	12 13	oveq12i	$⊢ ((A G C) G H) F ((B G D) G H) = (A G (C G H)) F (B G (D G H))$
15	11 14	eqtri	$⊢ ((A G C) F (B G D)) G H = (A G (C G H)) F (B G (D G H))$

Metamath Proof Explorer