Metamath Proof Explorer

Theorem mndpropd

Description: If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses mndpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
mndpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
mndpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
Assertion mndpropd ( 𝜑 → ( 𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd ) )

Proof

Step Hyp Ref Expression
1 mndpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 mndpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 mndpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 simplr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐾 ∈ Mnd )
5 simprl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
6 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
7 5 6 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
8 simprr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
9 8 6 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
12 10 11 mndcl ⊢ ( ( 𝐾 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
13 4 7 9 12 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
14 13 6 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
15 14 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Mnd ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
16 15 ex ⊢ ( 𝜑 → ( 𝐾 ∈ Mnd → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) )
17 simplr ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐿 ∈ Mnd )
18 simprl ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
19 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐿 ) )
20 18 19 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐿 ) )
21 simprr ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
22 21 19 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐿 ) )
23 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
24 eqid ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
25 23 24 mndcl ⊢ ( ( 𝐿 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) )
26 17 20 22 25 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) )
27 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
28 26 27 19 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
29 28 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐿 ∈ Mnd ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
30 29 ex ⊢ ( 𝜑 → ( 𝐿 ∈ Mnd → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) )
31 3 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) = ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) )
32 31 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) = ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) )
33 32 eleq1d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ↔ ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ) )
34 simplll ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝜑 )
35 simplrl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
36 simplrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 )
37 simpllr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
38 ovrspc2v ⊢ ( ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 )
39 35 36 37 38 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 )
40 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ 𝐵 )
41 3 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) )
42 34 39 40 41 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) )
43 34 35 36 31 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) = ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) )
44 43 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) )
45 42 44 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) )
46 ovrspc2v ⊢ ( ( ( 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
47 36 40 37 46 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
48 3 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) )
49 34 35 47 48 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) )
50 3 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) )
51 34 36 40 50 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) )
52 51 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) )
53 49 52 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) )
54 45 53 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ↔ ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) )
55 54 ralbidva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) )
56 33 55 anbi12d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
57 56 2ralbidva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
58 1 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝐾 ) )
59 58 eleq2d ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ↔ ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ) )
60 58 raleqdv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) )
61 59 60 anbi12d ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ) )
62 58 61 raleqbidv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ) )
63 58 62 raleqbidv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ) )
64 2 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝐿 ) )
65 64 eleq2d ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ↔ ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ) )
66 64 raleqdv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) )
67 65 66 anbi12d ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ↔ ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
68 64 67 raleqbidv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
69 64 68 raleqbidv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
70 57 63 69 3bitr3d ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ) )
71 simplll ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝜑 )
72 simplr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑠 ∈ 𝐵 )
73 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
74 3 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) )
75 71 72 73 74 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) )
76 75 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ↔ ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ) )
77 3 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ) ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) )
78 71 73 72 77 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) )
79 78 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ↔ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) )
80 76 79 anbi12d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ↔ ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ) )
81 80 ralbidva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ) )
82 81 rexbidva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ↔ ∃ 𝑠 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ) )
83 58 raleqdv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ) )
84 58 83 rexeqbidv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ↔ ∃ 𝑠 ∈ ( Base ‘ 𝐾 ) ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ) )
85 64 raleqdv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ) )
86 64 85 rexeqbidv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ↔ ∃ 𝑠 ∈ ( Base ‘ 𝐿 ) ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ) )
87 82 84 86 3bitr3d ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ( Base ‘ 𝐾 ) ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ↔ ∃ 𝑠 ∈ ( Base ‘ 𝐿 ) ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ) )
88 70 87 anbi12d ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( ( ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ∧ ∃ 𝑠 ∈ ( Base ‘ 𝐾 ) ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ) ↔ ( ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ∧ ∃ 𝑠 ∈ ( Base ‘ 𝐿 ) ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ) ) )
89 10 11 ismnd ⊢ ( 𝐾 ∈ Mnd ↔ ( ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ∀ 𝑣 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( 𝑢 ( +g ‘ 𝐾 ) 𝑣 ) ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐾 ) ( 𝑣 ( +g ‘ 𝐾 ) 𝑤 ) ) ) ∧ ∃ 𝑠 ∈ ( Base ‘ 𝐾 ) ∀ 𝑢 ∈ ( Base ‘ 𝐾 ) ( ( 𝑠 ( +g ‘ 𝐾 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐾 ) 𝑠 ) = 𝑢 ) ) )
90 23 24 ismnd ⊢ ( 𝐿 ∈ Mnd ↔ ( ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ∀ 𝑣 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( 𝑢 ( +g ‘ 𝐿 ) 𝑣 ) ( +g ‘ 𝐿 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝐿 ) ( 𝑣 ( +g ‘ 𝐿 ) 𝑤 ) ) ) ∧ ∃ 𝑠 ∈ ( Base ‘ 𝐿 ) ∀ 𝑢 ∈ ( Base ‘ 𝐿 ) ( ( 𝑠 ( +g ‘ 𝐿 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( +g ‘ 𝐿 ) 𝑠 ) = 𝑢 ) ) )
91 88 89 90 3bitr4g ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd ) )
92 91 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 → ( 𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd ) ) )
93 16 30 92 pm5.21ndd ⊢ ( 𝜑 → ( 𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd ) )