Step |
Hyp |
Ref |
Expression |
1 |
|
ring1.m |
⊢ 𝑀 = { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } |
2 |
|
eqid |
⊢ { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } = { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } |
3 |
2
|
grp1 |
⊢ ( 𝑍 ∈ 𝑉 → { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ∈ Grp ) |
4 |
|
snex |
⊢ { 𝑍 } ∈ V |
5 |
1
|
rngbase |
⊢ ( { 𝑍 } ∈ V → { 𝑍 } = ( Base ‘ 𝑀 ) ) |
6 |
4 5
|
ax-mp |
⊢ { 𝑍 } = ( Base ‘ 𝑀 ) |
7 |
6
|
eqcomi |
⊢ ( Base ‘ 𝑀 ) = { 𝑍 } |
8 |
|
snex |
⊢ { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ∈ V |
9 |
1
|
rngplusg |
⊢ ( { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ∈ V → { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } = ( +g ‘ 𝑀 ) ) |
10 |
9
|
eqcomd |
⊢ ( { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ∈ V → ( +g ‘ 𝑀 ) = { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ) |
11 |
8 10
|
ax-mp |
⊢ ( +g ‘ 𝑀 ) = { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } |
12 |
7 11 2
|
grppropstr |
⊢ ( 𝑀 ∈ Grp ↔ { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ∈ Grp ) |
13 |
3 12
|
sylibr |
⊢ ( 𝑍 ∈ 𝑉 → 𝑀 ∈ Grp ) |
14 |
2
|
mnd1 |
⊢ ( 𝑍 ∈ 𝑉 → { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ∈ Mnd ) |
15 |
|
eqid |
⊢ ( mulGrp ‘ 𝑀 ) = ( mulGrp ‘ 𝑀 ) |
16 |
15 6
|
mgpbas |
⊢ { 𝑍 } = ( Base ‘ ( mulGrp ‘ 𝑀 ) ) |
17 |
2
|
grpbase |
⊢ ( { 𝑍 } ∈ V → { 𝑍 } = ( Base ‘ { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ) ) |
18 |
4 17
|
ax-mp |
⊢ { 𝑍 } = ( Base ‘ { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ) |
19 |
16 18
|
eqtr3i |
⊢ ( Base ‘ ( mulGrp ‘ 𝑀 ) ) = ( Base ‘ { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ) |
20 |
1
|
rngmulr |
⊢ ( { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ∈ V → { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } = ( .r ‘ 𝑀 ) ) |
21 |
8 20
|
ax-mp |
⊢ { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } = ( .r ‘ 𝑀 ) |
22 |
2
|
grpplusg |
⊢ ( { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ∈ V → { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } = ( +g ‘ { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ) ) |
23 |
8 22
|
ax-mp |
⊢ { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } = ( +g ‘ { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ) |
24 |
|
eqid |
⊢ ( .r ‘ 𝑀 ) = ( .r ‘ 𝑀 ) |
25 |
15 24
|
mgpplusg |
⊢ ( .r ‘ 𝑀 ) = ( +g ‘ ( mulGrp ‘ 𝑀 ) ) |
26 |
21 23 25
|
3eqtr3ri |
⊢ ( +g ‘ ( mulGrp ‘ 𝑀 ) ) = ( +g ‘ { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ) |
27 |
19 26
|
mndprop |
⊢ ( ( mulGrp ‘ 𝑀 ) ∈ Mnd ↔ { 〈 ( Base ‘ ndx ) , { 𝑍 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 〉 } ∈ Mnd ) |
28 |
14 27
|
sylibr |
⊢ ( 𝑍 ∈ 𝑉 → ( mulGrp ‘ 𝑀 ) ∈ Mnd ) |
29 |
|
df-ov |
⊢ ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) = ( { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ‘ 〈 𝑍 , 𝑍 〉 ) |
30 |
|
opex |
⊢ 〈 𝑍 , 𝑍 〉 ∈ V |
31 |
|
fvsng |
⊢ ( ( 〈 𝑍 , 𝑍 〉 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ‘ 〈 𝑍 , 𝑍 〉 ) = 𝑍 ) |
32 |
30 31
|
mpan |
⊢ ( 𝑍 ∈ 𝑉 → ( { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ‘ 〈 𝑍 , 𝑍 〉 ) = 𝑍 ) |
33 |
29 32
|
eqtrid |
⊢ ( 𝑍 ∈ 𝑉 → ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) = 𝑍 ) |
34 |
33
|
oveq2d |
⊢ ( 𝑍 ∈ 𝑉 → ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) |
35 |
33 33
|
oveq12d |
⊢ ( 𝑍 ∈ 𝑉 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) |
36 |
34 35
|
eqtr4d |
⊢ ( 𝑍 ∈ 𝑉 → ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) |
37 |
33
|
oveq1d |
⊢ ( 𝑍 ∈ 𝑉 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) |
38 |
37 35
|
eqtr4d |
⊢ ( 𝑍 ∈ 𝑉 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) |
39 |
|
oveq1 |
⊢ ( 𝑎 = 𝑍 → ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) |
40 |
|
oveq1 |
⊢ ( 𝑎 = 𝑍 → ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) ) |
41 |
|
oveq1 |
⊢ ( 𝑎 = 𝑍 → ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) |
42 |
40 41
|
oveq12d |
⊢ ( 𝑎 = 𝑍 → ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) |
43 |
39 42
|
eqeq12d |
⊢ ( 𝑎 = 𝑍 → ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ↔ ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) |
44 |
40
|
oveq1d |
⊢ ( 𝑎 = 𝑍 → ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) |
45 |
41
|
oveq1d |
⊢ ( 𝑎 = 𝑍 → ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) |
46 |
44 45
|
eqeq12d |
⊢ ( 𝑎 = 𝑍 → ( ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ↔ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) |
47 |
43 46
|
anbi12d |
⊢ ( 𝑎 = 𝑍 → ( ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ↔ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) ) |
48 |
47
|
2ralbidv |
⊢ ( 𝑎 = 𝑍 → ( ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ↔ ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) ) |
49 |
48
|
ralsng |
⊢ ( 𝑍 ∈ 𝑉 → ( ∀ 𝑎 ∈ { 𝑍 } ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ↔ ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) ) |
50 |
|
oveq1 |
⊢ ( 𝑏 = 𝑍 → ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) |
51 |
50
|
oveq2d |
⊢ ( 𝑏 = 𝑍 → ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) |
52 |
|
oveq2 |
⊢ ( 𝑏 = 𝑍 → ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) |
53 |
52
|
oveq1d |
⊢ ( 𝑏 = 𝑍 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) |
54 |
51 53
|
eqeq12d |
⊢ ( 𝑏 = 𝑍 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ↔ ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) |
55 |
52
|
oveq1d |
⊢ ( 𝑏 = 𝑍 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) |
56 |
50
|
oveq2d |
⊢ ( 𝑏 = 𝑍 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) |
57 |
55 56
|
eqeq12d |
⊢ ( 𝑏 = 𝑍 → ( ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ↔ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) |
58 |
54 57
|
anbi12d |
⊢ ( 𝑏 = 𝑍 → ( ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ↔ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) ) |
59 |
58
|
ralbidv |
⊢ ( 𝑏 = 𝑍 → ( ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ↔ ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) ) |
60 |
59
|
ralsng |
⊢ ( 𝑍 ∈ 𝑉 → ( ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ↔ ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) ) |
61 |
|
oveq2 |
⊢ ( 𝑐 = 𝑍 → ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) |
62 |
61
|
oveq2d |
⊢ ( 𝑐 = 𝑍 → ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) |
63 |
61
|
oveq2d |
⊢ ( 𝑐 = 𝑍 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) |
64 |
62 63
|
eqeq12d |
⊢ ( 𝑐 = 𝑍 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ↔ ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) ) |
65 |
|
oveq2 |
⊢ ( 𝑐 = 𝑍 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) |
66 |
61 61
|
oveq12d |
⊢ ( 𝑐 = 𝑍 → ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) |
67 |
65 66
|
eqeq12d |
⊢ ( 𝑐 = 𝑍 → ( ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ↔ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) ) |
68 |
64 67
|
anbi12d |
⊢ ( 𝑐 = 𝑍 → ( ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ↔ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) ) ) |
69 |
68
|
ralsng |
⊢ ( 𝑍 ∈ 𝑉 → ( ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ↔ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) ) ) |
70 |
49 60 69
|
3bitrd |
⊢ ( 𝑍 ∈ 𝑉 → ( ∀ 𝑎 ∈ { 𝑍 } ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ↔ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ∧ ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) = ( ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑍 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑍 ) ) ) ) ) |
71 |
36 38 70
|
mpbir2and |
⊢ ( 𝑍 ∈ 𝑉 → ∀ 𝑎 ∈ { 𝑍 } ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) |
72 |
8 9
|
ax-mp |
⊢ { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } = ( +g ‘ 𝑀 ) |
73 |
6 15 72 21
|
isring |
⊢ ( 𝑀 ∈ Ring ↔ ( 𝑀 ∈ Grp ∧ ( mulGrp ‘ 𝑀 ) ∈ Mnd ∧ ∀ 𝑎 ∈ { 𝑍 } ∀ 𝑏 ∈ { 𝑍 } ∀ 𝑐 ∈ { 𝑍 } ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ∧ ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑏 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) = ( ( 𝑎 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } ( 𝑏 { 〈 〈 𝑍 , 𝑍 〉 , 𝑍 〉 } 𝑐 ) ) ) ) ) |
74 |
13 28 71 73
|
syl3anbrc |
⊢ ( 𝑍 ∈ 𝑉 → 𝑀 ∈ Ring ) |