grpoidinvlem3

Description: Lemma for grpoidinv . (Contributed by NM, 11-Oct-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpfo.1	$⊢ X = ran G$
	grpidinvlem3.2	$⊢ φ \leftrightarrow \forall x \in X U G x = x$
	grpidinvlem3.3	$⊢ ψ \leftrightarrow \forall x \in X \exists z \in X z G x = U$
Assertion	grpoidinvlem3	$⊢ (((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \to \exists y \in X (y G A = U \land A G y = U)$

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	$⊢ X = ran G$
2		grpidinvlem3.2	$⊢ φ \leftrightarrow \forall x \in X U G x = x$
3		grpidinvlem3.3	$⊢ ψ \leftrightarrow \forall x \in X \exists z \in X z G x = U$
4		oveq1	$⊢ z = y \to z G x = y G x$
5	4	eqeq1d	$⊢ z = y \to (z G x = U \leftrightarrow y G x = U)$
6	5	cbvrexvw	$⊢ \exists z \in X z G x = U \leftrightarrow \exists y \in X y G x = U$
7	6	ralbii	$⊢ \forall x \in X \exists z \in X z G x = U \leftrightarrow \forall x \in X \exists y \in X y G x = U$
8	3 7	bitri	$⊢ ψ \leftrightarrow \forall x \in X \exists y \in X y G x = U$
9		oveq2	$⊢ x = A \to y G x = y G A$
10	9	eqeq1d	$⊢ x = A \to (y G x = U \leftrightarrow y G A = U)$
11	10	rexbidv	$⊢ x = A \to (\exists y \in X y G x = U \leftrightarrow \exists y \in X y G A = U)$
12	11	rspccva	$⊢ (\forall x \in X \exists y \in X y G x = U \land A \in X) \to \exists y \in X y G A = U$
13	8 12	sylanb	$⊢ (ψ \land A \in X) \to \exists y \in X y G A = U$
14	13	adantll	$⊢ ((φ \land ψ) \land A \in X) \to \exists y \in X y G A = U$
15	14	adantll	$⊢ (((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \to \exists y \in X y G A = U$
16	1	grpocl	$⊢ (G \in GrpOp \land A \in X \land y \in X) \to A G y \in X$
17	16	3expa	$⊢ ((G \in GrpOp \land A \in X) \land y \in X) \to A G y \in X$
18	17	adantllr	$⊢ (((G \in GrpOp \land U \in X) \land A \in X) \land y \in X) \to A G y \in X$
19	18	adantllr	$⊢ ((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \to A G y \in X$
20	2	biimpi	$⊢ φ \to \forall x \in X U G x = x$
21	20	ad2antrl	$⊢ ((G \in GrpOp \land U \in X) \land (φ \land ψ)) \to \forall x \in X U G x = x$
22	21	ad2antrr	$⊢ ((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \to \forall x \in X U G x = x$
23		oveq2	$⊢ x = A G y \to U G x = U G (A G y)$
24		id	$⊢ x = A G y \to x = A G y$
25	23 24	eqeq12d	$⊢ x = A G y \to (U G x = x \leftrightarrow U G (A G y) = A G y)$
26	25	rspcva	$⊢ (A G y \in X \land \forall x \in X U G x = x) \to U G (A G y) = A G y$
27	19 22 26	syl2anc	$⊢ ((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \to U G (A G y) = A G y$
28	27	adantr	$⊢ (((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \land y G A = U) \to U G (A G y) = A G y$
29		pm3.22	$⊢ ((y \in X \land A \in X) \land G \in GrpOp) \to (G \in GrpOp \land (y \in X \land A \in X))$
30	29	an31s	$⊢ ((G \in GrpOp \land A \in X) \land y \in X) \to (G \in GrpOp \land (y \in X \land A \in X))$
31	30	adantllr	$⊢ (((G \in GrpOp \land U \in X) \land A \in X) \land y \in X) \to (G \in GrpOp \land (y \in X \land A \in X))$
32	31	adantllr	$⊢ ((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \to (G \in GrpOp \land (y \in X \land A \in X))$
33	32	adantr	$⊢ (((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \land y G A = U) \to (G \in GrpOp \land (y \in X \land A \in X))$
34		oveq2	$⊢ x = y \to U G x = U G y$
35		id	$⊢ x = y \to x = y$
36	34 35	eqeq12d	$⊢ x = y \to (U G x = x \leftrightarrow U G y = y)$
37	36	rspccva	$⊢ (\forall x \in X U G x = x \land y \in X) \to U G y = y$
38	2 37	sylanb	$⊢ (φ \land y \in X) \to U G y = y$
39	38	adantlr	$⊢ ((φ \land ψ) \land y \in X) \to U G y = y$
40	39	adantlr	$⊢ (((φ \land ψ) \land A \in X) \land y \in X) \to U G y = y$
41	40	adantlll	$⊢ ((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \to U G y = y$
42	41	anim1i	$⊢ (((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \land y G A = U) \to (U G y = y \land y G A = U)$
43	1	grpoidinvlem2	$⊢ ((G \in GrpOp \land (y \in X \land A \in X)) \land (U G y = y \land y G A = U)) \to (A G y) G (A G y) = A G y$
44	33 42 43	syl2anc	$⊢ (((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \land y G A = U) \to (A G y) G (A G y) = A G y$
45	16	3expb	$⊢ (G \in GrpOp \land (A \in X \land y \in X)) \to A G y \in X$
46	45	ad2ant2rl	$⊢ ((G \in GrpOp \land U \in X) \land (φ \land (A \in X \land y \in X))) \to A G y \in X$
47		oveq1	$⊢ z = w \to z G x = w G x$
48	47	eqeq1d	$⊢ z = w \to (z G x = U \leftrightarrow w G x = U)$
49	48	cbvrexvw	$⊢ \exists z \in X z G x = U \leftrightarrow \exists w \in X w G x = U$
50	49	ralbii	$⊢ \forall x \in X \exists z \in X z G x = U \leftrightarrow \forall x \in X \exists w \in X w G x = U$
51	3 50	bitri	$⊢ ψ \leftrightarrow \forall x \in X \exists w \in X w G x = U$
52		oveq2	$⊢ x = A G y \to w G x = w G (A G y)$
53	52	eqeq1d	$⊢ x = A G y \to (w G x = U \leftrightarrow w G (A G y) = U)$
54	53	rexbidv	$⊢ x = A G y \to (\exists w \in X w G x = U \leftrightarrow \exists w \in X w G (A G y) = U)$
55	54	rspcva	$⊢ (A G y \in X \land \forall x \in X \exists w \in X w G x = U) \to \exists w \in X w G (A G y) = U$
56	51 55	sylan2b	$⊢ (A G y \in X \land ψ) \to \exists w \in X w G (A G y) = U$
57		anass	$⊢ ((G \in GrpOp \land w \in X) \land A G y \in X) \leftrightarrow (G \in GrpOp \land (w \in X \land A G y \in X))$
58	57	biimpi	$⊢ ((G \in GrpOp \land w \in X) \land A G y \in X) \to (G \in GrpOp \land (w \in X \land A G y \in X))$
59	58	an32s	$⊢ ((G \in GrpOp \land A G y \in X) \land w \in X) \to (G \in GrpOp \land (w \in X \land A G y \in X))$
60	59	ex	$⊢ (G \in GrpOp \land A G y \in X) \to (w \in X \to (G \in GrpOp \land (w \in X \land A G y \in X)))$
61	45 60	syldan	$⊢ (G \in GrpOp \land (A \in X \land y \in X)) \to (w \in X \to (G \in GrpOp \land (w \in X \land A G y \in X)))$
62	61	ad2ant2rl	$⊢ ((G \in GrpOp \land U \in X) \land (φ \land (A \in X \land y \in X))) \to (w \in X \to (G \in GrpOp \land (w \in X \land A G y \in X)))$
63	62	imp	$⊢ (((G \in GrpOp \land U \in X) \land (φ \land (A \in X \land y \in X))) \land w \in X) \to (G \in GrpOp \land (w \in X \land A G y \in X))$
64	1	grpoidinvlem1	$⊢ ((G \in GrpOp \land (w \in X \land A G y \in X)) \land (w G (A G y) = U \land (A G y) G (A G y) = A G y)) \to U G (A G y) = U$
65	63 64	sylan	$⊢ ((((G \in GrpOp \land U \in X) \land (φ \land (A \in X \land y \in X))) \land w \in X) \land (w G (A G y) = U \land (A G y) G (A G y) = A G y)) \to U G (A G y) = U$
66	65	exp43	$⊢ ((G \in GrpOp \land U \in X) \land (φ \land (A \in X \land y \in X))) \to (w \in X \to (w G (A G y) = U \to ((A G y) G (A G y) = A G y \to U G (A G y) = U)))$
67	66	rexlimdv	$⊢ ((G \in GrpOp \land U \in X) \land (φ \land (A \in X \land y \in X))) \to (\exists w \in X w G (A G y) = U \to ((A G y) G (A G y) = A G y \to U G (A G y) = U))$
68	56 67	syl5	$⊢ ((G \in GrpOp \land U \in X) \land (φ \land (A \in X \land y \in X))) \to ((A G y \in X \land ψ) \to ((A G y) G (A G y) = A G y \to U G (A G y) = U))$
69	46 68	mpand	$⊢ ((G \in GrpOp \land U \in X) \land (φ \land (A \in X \land y \in X))) \to (ψ \to ((A G y) G (A G y) = A G y \to U G (A G y) = U))$
70	69	exp32	$⊢ (G \in GrpOp \land U \in X) \to (φ \to ((A \in X \land y \in X) \to (ψ \to ((A G y) G (A G y) = A G y \to U G (A G y) = U))))$
71	70	com34	$⊢ (G \in GrpOp \land U \in X) \to (φ \to (ψ \to ((A \in X \land y \in X) \to ((A G y) G (A G y) = A G y \to U G (A G y) = U))))$
72	71	imp32	$⊢ ((G \in GrpOp \land U \in X) \land (φ \land ψ)) \to ((A \in X \land y \in X) \to ((A G y) G (A G y) = A G y \to U G (A G y) = U))$
73	72	impl	$⊢ ((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \to ((A G y) G (A G y) = A G y \to U G (A G y) = U)$
74	73	adantr	$⊢ (((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \land y G A = U) \to ((A G y) G (A G y) = A G y \to U G (A G y) = U)$
75	44 74	mpd	$⊢ (((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \land y G A = U) \to U G (A G y) = U$
76	28 75	eqtr3d	$⊢ (((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \land y G A = U) \to A G y = U$
77	76	ex	$⊢ ((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \to (y G A = U \to A G y = U)$
78	77	ancld	$⊢ ((((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \land y \in X) \to (y G A = U \to (y G A = U \land A G y = U))$
79	78	reximdva	$⊢ (((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \to (\exists y \in X y G A = U \to \exists y \in X (y G A = U \land A G y = U))$
80	15 79	mpd	$⊢ (((G \in GrpOp \land U \in X) \land (φ \land ψ)) \land A \in X) \to \exists y \in X (y G A = U \land A G y = U)$

Metamath Proof Explorer

Theorem grpoidinvlem3

Proof