Step |
Hyp |
Ref |
Expression |
1 |
|
frgpup.b |
⊢ 𝐵 = ( Base ‘ 𝐻 ) |
2 |
|
frgpup.n |
⊢ 𝑁 = ( invg ‘ 𝐻 ) |
3 |
|
frgpup.t |
⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) |
4 |
|
frgpup.h |
⊢ ( 𝜑 → 𝐻 ∈ Grp ) |
5 |
|
frgpup.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
6 |
|
frgpup.a |
⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 ) |
7 |
|
frgpuptinv.m |
⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ) |
8 |
|
elxp2 |
⊢ ( 𝐴 ∈ ( 𝐼 × 2o ) ↔ ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 2o 𝐴 = 〈 𝑎 , 𝑏 〉 ) |
9 |
7
|
efgmval |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑎 𝑀 𝑏 ) = 〈 𝑎 , ( 1o ∖ 𝑏 ) 〉 ) |
10 |
9
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑎 𝑀 𝑏 ) = 〈 𝑎 , ( 1o ∖ 𝑏 ) 〉 ) |
11 |
10
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑇 ‘ 〈 𝑎 , ( 1o ∖ 𝑏 ) 〉 ) ) |
12 |
|
df-ov |
⊢ ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑇 ‘ 〈 𝑎 , ( 1o ∖ 𝑏 ) 〉 ) |
13 |
11 12
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) ) |
14 |
|
elpri |
⊢ ( 𝑏 ∈ { ∅ , 1o } → ( 𝑏 = ∅ ∨ 𝑏 = 1o ) ) |
15 |
|
df2o3 |
⊢ 2o = { ∅ , 1o } |
16 |
14 15
|
eleq2s |
⊢ ( 𝑏 ∈ 2o → ( 𝑏 = ∅ ∨ 𝑏 = 1o ) ) |
17 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝑎 ∈ 𝐼 ) |
18 |
|
1oex |
⊢ 1o ∈ V |
19 |
18
|
prid2 |
⊢ 1o ∈ { ∅ , 1o } |
20 |
19 15
|
eleqtrri |
⊢ 1o ∈ 2o |
21 |
|
1n0 |
⊢ 1o ≠ ∅ |
22 |
|
neeq1 |
⊢ ( 𝑧 = 1o → ( 𝑧 ≠ ∅ ↔ 1o ≠ ∅ ) ) |
23 |
21 22
|
mpbiri |
⊢ ( 𝑧 = 1o → 𝑧 ≠ ∅ ) |
24 |
|
ifnefalse |
⊢ ( 𝑧 ≠ ∅ → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) |
25 |
23 24
|
syl |
⊢ ( 𝑧 = 1o → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) |
26 |
|
fveq2 |
⊢ ( 𝑦 = 𝑎 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) ) |
27 |
26
|
fveq2d |
⊢ ( 𝑦 = 𝑎 → ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) ) |
28 |
25 27
|
sylan9eqr |
⊢ ( ( 𝑦 = 𝑎 ∧ 𝑧 = 1o ) → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) ) |
29 |
|
fvex |
⊢ ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) ∈ V |
30 |
28 3 29
|
ovmpoa |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 1o ∈ 2o ) → ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) ) |
31 |
17 20 30
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) ) |
32 |
|
0ex |
⊢ ∅ ∈ V |
33 |
32
|
prid1 |
⊢ ∅ ∈ { ∅ , 1o } |
34 |
33 15
|
eleqtrri |
⊢ ∅ ∈ 2o |
35 |
|
iftrue |
⊢ ( 𝑧 = ∅ → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝑦 ) ) |
36 |
35 26
|
sylan9eqr |
⊢ ( ( 𝑦 = 𝑎 ∧ 𝑧 = ∅ ) → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝑎 ) ) |
37 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑎 ) ∈ V |
38 |
36 3 37
|
ovmpoa |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ( 𝑎 𝑇 ∅ ) = ( 𝐹 ‘ 𝑎 ) ) |
39 |
17 34 38
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 ∅ ) = ( 𝐹 ‘ 𝑎 ) ) |
40 |
39
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) ) |
41 |
31 40
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) |
42 |
|
difeq2 |
⊢ ( 𝑏 = ∅ → ( 1o ∖ 𝑏 ) = ( 1o ∖ ∅ ) ) |
43 |
|
dif0 |
⊢ ( 1o ∖ ∅ ) = 1o |
44 |
42 43
|
eqtrdi |
⊢ ( 𝑏 = ∅ → ( 1o ∖ 𝑏 ) = 1o ) |
45 |
44
|
oveq2d |
⊢ ( 𝑏 = ∅ → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑎 𝑇 1o ) ) |
46 |
|
oveq2 |
⊢ ( 𝑏 = ∅ → ( 𝑎 𝑇 𝑏 ) = ( 𝑎 𝑇 ∅ ) ) |
47 |
46
|
fveq2d |
⊢ ( 𝑏 = ∅ → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) |
48 |
45 47
|
eqeq12d |
⊢ ( 𝑏 = ∅ → ( ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ↔ ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) ) |
49 |
41 48
|
syl5ibrcom |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑏 = ∅ → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) ) |
50 |
41
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) = ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) ) |
51 |
6
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 ) |
52 |
39 51
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 ∅ ) ∈ 𝐵 ) |
53 |
1 2
|
grpinvinv |
⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑎 𝑇 ∅ ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) = ( 𝑎 𝑇 ∅ ) ) |
54 |
4 52 53
|
syl2an2r |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) = ( 𝑎 𝑇 ∅ ) ) |
55 |
50 54
|
eqtr2d |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 ∅ ) = ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) ) |
56 |
|
difeq2 |
⊢ ( 𝑏 = 1o → ( 1o ∖ 𝑏 ) = ( 1o ∖ 1o ) ) |
57 |
|
difid |
⊢ ( 1o ∖ 1o ) = ∅ |
58 |
56 57
|
eqtrdi |
⊢ ( 𝑏 = 1o → ( 1o ∖ 𝑏 ) = ∅ ) |
59 |
58
|
oveq2d |
⊢ ( 𝑏 = 1o → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑎 𝑇 ∅ ) ) |
60 |
|
oveq2 |
⊢ ( 𝑏 = 1o → ( 𝑎 𝑇 𝑏 ) = ( 𝑎 𝑇 1o ) ) |
61 |
60
|
fveq2d |
⊢ ( 𝑏 = 1o → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) ) |
62 |
59 61
|
eqeq12d |
⊢ ( 𝑏 = 1o → ( ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ↔ ( 𝑎 𝑇 ∅ ) = ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) ) ) |
63 |
55 62
|
syl5ibrcom |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑏 = 1o → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) ) |
64 |
49 63
|
jaod |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑏 = ∅ ∨ 𝑏 = 1o ) → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) ) |
65 |
16 64
|
syl5 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑏 ∈ 2o → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) ) |
66 |
65
|
impr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) |
67 |
13 66
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) |
68 |
|
fveq2 |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ 〈 𝑎 , 𝑏 〉 ) ) |
69 |
|
df-ov |
⊢ ( 𝑎 𝑀 𝑏 ) = ( 𝑀 ‘ 〈 𝑎 , 𝑏 〉 ) |
70 |
68 69
|
eqtr4di |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑀 ‘ 𝐴 ) = ( 𝑎 𝑀 𝑏 ) ) |
71 |
70
|
fveq2d |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) ) |
72 |
|
fveq2 |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑇 ‘ 𝐴 ) = ( 𝑇 ‘ 〈 𝑎 , 𝑏 〉 ) ) |
73 |
|
df-ov |
⊢ ( 𝑎 𝑇 𝑏 ) = ( 𝑇 ‘ 〈 𝑎 , 𝑏 〉 ) |
74 |
72 73
|
eqtr4di |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑇 ‘ 𝐴 ) = ( 𝑎 𝑇 𝑏 ) ) |
75 |
74
|
fveq2d |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) |
76 |
71 75
|
eqeq12d |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) ↔ ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) ) |
77 |
67 76
|
syl5ibrcom |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) ) ) |
78 |
77
|
rexlimdvva |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 2o 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) ) ) |
79 |
8 78
|
syl5bi |
⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐼 × 2o ) → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) ) ) |
80 |
79
|
imp |
⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐼 × 2o ) ) → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) ) |