caonncan

Description: Transfer nncan -shaped laws to vectors of numbers. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	caonncan.i	$⊢ φ \to I \in V$
	caonncan.a	$⊢ φ \to A : I ⟶ S$
	caonncan.b	$⊢ φ \to B : I ⟶ S$
	caonncan.z	$⊢ (φ \land (x \in S \land y \in S)) \to x M (x M y) = y$
Assertion	caonncan	$⊢ φ \to A M_{f} (A M_{f} B) = B$

Proof

Step	Hyp	Ref	Expression
1		caonncan.i	$⊢ φ \to I \in V$
2		caonncan.a	$⊢ φ \to A : I ⟶ S$
3		caonncan.b	$⊢ φ \to B : I ⟶ S$
4		caonncan.z	$⊢ (φ \land (x \in S \land y \in S)) \to x M (x M y) = y$
5	2	ffvelcdmda	$⊢ (φ \land z \in I) \to A (z) \in S$
6	3	ffvelcdmda	$⊢ (φ \land z \in I) \to B (z) \in S$
7	4	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in S x M (x M y) = y$
8	7	adantr	$⊢ (φ \land z \in I) \to \forall x \in S \forall y \in S x M (x M y) = y$
9		id	$⊢ x = A (z) \to x = A (z)$
10		oveq1	$⊢ x = A (z) \to x M y = A (z) M y$
11	9 10	oveq12d	$⊢ x = A (z) \to x M (x M y) = A (z) M (A (z) M y)$
12	11	eqeq1d	$⊢ x = A (z) \to (x M (x M y) = y \leftrightarrow A (z) M (A (z) M y) = y)$
13		oveq2	$⊢ y = B (z) \to A (z) M y = A (z) M B (z)$
14	13	oveq2d	$⊢ y = B (z) \to A (z) M (A (z) M y) = A (z) M (A (z) M B (z))$
15		id	$⊢ y = B (z) \to y = B (z)$
16	14 15	eqeq12d	$⊢ y = B (z) \to (A (z) M (A (z) M y) = y \leftrightarrow A (z) M (A (z) M B (z)) = B (z))$
17	12 16	rspc2va	$⊢ ((A (z) \in S \land B (z) \in S) \land \forall x \in S \forall y \in S x M (x M y) = y) \to A (z) M (A (z) M B (z)) = B (z)$
18	5 6 8 17	syl21anc	$⊢ (φ \land z \in I) \to A (z) M (A (z) M B (z)) = B (z)$
19	18	mpteq2dva	$⊢ φ \to (z \in I ⟼ A (z) M (A (z) M B (z))) = (z \in I ⟼ B (z))$
20		fvexd	$⊢ (φ \land z \in I) \to A (z) \in V$
21		ovexd	$⊢ (φ \land z \in I) \to A (z) M B (z) \in V$
22	2	feqmptd	$⊢ φ \to A = (z \in I ⟼ A (z))$
23		fvexd	$⊢ (φ \land z \in I) \to B (z) \in V$
24	3	feqmptd	$⊢ φ \to B = (z \in I ⟼ B (z))$
25	1 20 23 22 24	offval2	$⊢ φ \to A M_{f} B = (z \in I ⟼ A (z) M B (z))$
26	1 20 21 22 25	offval2	$⊢ φ \to A M_{f} (A M_{f} B) = (z \in I ⟼ A (z) M (A (z) M B (z)))$
27	19 26 24	3eqtr4d	$⊢ φ \to A M_{f} (A M_{f} B) = B$

Metamath Proof Explorer

Theorem caonncan

Proof