# Metamath Proof Explorer

## Theorem grpoidinvlem3

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

Ref Expression
Hypotheses grpfo.1 𝑋 = ran 𝐺
grpidinvlem3.2 ( 𝜑 ↔ ∀ 𝑥𝑋 ( 𝑈 𝐺 𝑥 ) = 𝑥 )
grpidinvlem3.3 ( 𝜓 ↔ ∀ 𝑥𝑋𝑧𝑋 ( 𝑧 𝐺 𝑥 ) = 𝑈 )
Assertion grpoidinvlem3 ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈𝑋 ) ∧ ( 𝜑𝜓 ) ) ∧ 𝐴𝑋 ) → ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) )

### Proof

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