Step |
Hyp |
Ref |
Expression |
1 |
|
lsmcomx.v |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
lsmcomx.s |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
3 |
|
simpl1 |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝐺 ∈ Abel ) |
4 |
|
simpl2 |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑇 ⊆ 𝐵 ) |
5 |
|
simprl |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑇 ) |
6 |
4 5
|
sseldd |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑦 ∈ 𝐵 ) |
7 |
|
simpl3 |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑈 ⊆ 𝐵 ) |
8 |
|
simprr |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑧 ∈ 𝑈 ) |
9 |
7 8
|
sseldd |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑧 ∈ 𝐵 ) |
10 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
11 |
1 10
|
ablcom |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) |
12 |
3 6 9 11
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) |
13 |
12
|
eqeq2d |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ↔ 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) ) |
14 |
13
|
2rexbidva |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) ) |
15 |
|
rexcom |
⊢ ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑧 ∈ 𝑈 ∃ 𝑦 ∈ 𝑇 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) |
16 |
14 15
|
bitrdi |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑧 ∈ 𝑈 ∃ 𝑦 ∈ 𝑇 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) ) |
17 |
1 10 2
|
lsmelvalx |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) |
18 |
1 10 2
|
lsmelvalx |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑈 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑈 ⊕ 𝑇 ) ↔ ∃ 𝑧 ∈ 𝑈 ∃ 𝑦 ∈ 𝑇 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) ) |
19 |
18
|
3com23 |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑈 ⊕ 𝑇 ) ↔ ∃ 𝑧 ∈ 𝑈 ∃ 𝑦 ∈ 𝑇 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) ) |
20 |
16 17 19
|
3bitr4d |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ 𝑥 ∈ ( 𝑈 ⊕ 𝑇 ) ) ) |
21 |
20
|
eqrdv |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) ) |