Theorem caovlem2 7670

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

Hypotheses

Ref	Expression
caovdir.1	⊢ 𝐴 ∈ V
caovdir.2	⊢ 𝐵 ∈ V
caovdir.3	⊢ 𝐶 ∈ V
caovdir.com	⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)
caovdir.distr	⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))
caovdl.4	⊢ 𝐷 ∈ V
caovdl.5	⊢ 𝐻 ∈ V
caovdl.ass	⊢ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))
caovdl2.6	⊢ 𝑅 ∈ V
caovdl2.com	⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
caovdl2.ass	⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))

Assertion

Ref	Expression
caovlem2	⊢ ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻))))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑥,𝐷,𝑦,𝑧   𝑥,𝐹,𝑦,𝑧   𝑥,𝐺,𝑦,𝑧   𝑥,𝐻,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧

Proof of Theorem caovlem2

Step	Hyp	Ref	Expression
1		ovex 7465	. . 3 ⊢ (𝐴𝐺(𝐶𝐺𝐻)) ∈ V
2		ovex 7465	. . 3 ⊢ (𝐵𝐺(𝐷𝐺𝐻)) ∈ V
3		ovex 7465	. . 3 ⊢ (𝐴𝐺(𝐷𝐺𝑅)) ∈ V
4		caovdl2.com	. . 3 ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
5		caovdl2.ass	. . 3 ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))
6		ovex 7465	. . 3 ⊢ (𝐵𝐺(𝐶𝐺𝑅)) ∈ V
7	1, 2, 3, 4, 5, 6	caov42 7667	. 2 ⊢ (((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻)))𝐹((𝐴𝐺(𝐷𝐺𝑅))𝐹(𝐵𝐺(𝐶𝐺𝑅)))) = (((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐴𝐺(𝐷𝐺𝑅)))𝐹((𝐵𝐺(𝐶𝐺𝑅))𝐹(𝐵𝐺(𝐷𝐺𝐻))))
8		caovdir.1	. . . 4 ⊢ 𝐴 ∈ V
9		caovdir.2	. . . 4 ⊢ 𝐵 ∈ V
10		caovdir.3	. . . 4 ⊢ 𝐶 ∈ V
11		caovdir.com	. . . 4 ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥)
12		caovdir.distr	. . . 4 ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))
13		caovdl.4	. . . 4 ⊢ 𝐷 ∈ V
14		caovdl.5	. . . 4 ⊢ 𝐻 ∈ V
15		caovdl.ass	. . . 4 ⊢ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))
16	8, 9, 10, 11, 12, 13, 14, 15	caovdilem 7669	. . 3 ⊢ (((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻) = ((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻)))
17		caovdl2.6	. . . 4 ⊢ 𝑅 ∈ V
18	8, 9, 13, 11, 12, 10, 17, 15	caovdilem 7669	. . 3 ⊢ (((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅) = ((𝐴𝐺(𝐷𝐺𝑅))𝐹(𝐵𝐺(𝐶𝐺𝑅)))
19	16, 18	oveq12i 7444	. 2 ⊢ ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = (((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻)))𝐹((𝐴𝐺(𝐷𝐺𝑅))𝐹(𝐵𝐺(𝐶𝐺𝑅))))
20		ovex 7465	. . . 4 ⊢ (𝐶𝐺𝐻) ∈ V
21		ovex 7465	. . . 4 ⊢ (𝐷𝐺𝑅) ∈ V
22	8, 20, 21, 12	caovdi 7653	. . 3 ⊢ (𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅))) = ((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐴𝐺(𝐷𝐺𝑅)))
23		ovex 7465	. . . 4 ⊢ (𝐶𝐺𝑅) ∈ V
24		ovex 7465	. . . 4 ⊢ (𝐷𝐺𝐻) ∈ V
25	9, 23, 24, 12	caovdi 7653	. . 3 ⊢ (𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻))) = ((𝐵𝐺(𝐶𝐺𝑅))𝐹(𝐵𝐺(𝐷𝐺𝐻)))
26	22, 25	oveq12i 7444	. 2 ⊢ ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))) = (((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐴𝐺(𝐷𝐺𝑅)))𝐹((𝐵𝐺(𝐶𝐺𝑅))𝐹(𝐵𝐺(𝐷𝐺𝐻))))
27	7, 19, 26	3eqtr4i 2774	1 ⊢ ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻))))

Syntax hints:   = wceq 1539   ∈ wcel 2107  Vcvv 3479  (class class class)co 7432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-nul 5305

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435

This theorem is referenced by:  mulasssr  11131