Step |
Hyp |
Ref |
Expression |
1 |
|
pj1eu.a |
⊢ + = ( +g ‘ 𝐺 ) |
2 |
|
pj1eu.s |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
3 |
|
pj1eu.o |
⊢ 0 = ( 0g ‘ 𝐺 ) |
4 |
|
pj1eu.z |
⊢ 𝑍 = ( Cntz ‘ 𝐺 ) |
5 |
|
pj1eu.2 |
⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) |
6 |
|
pj1eu.3 |
⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) |
7 |
|
pj1eu.4 |
⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } ) |
8 |
|
pj1eu.5 |
⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) |
9 |
|
pj1f.p |
⊢ 𝑃 = ( proj1 ‘ 𝐺 ) |
10 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) |
11 |
|
subgrcl |
⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) |
12 |
10 11
|
syl |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝐺 ∈ Grp ) |
13 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
14 |
13
|
subgss |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) ) |
15 |
6 14
|
syl |
⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐺 ) ) |
16 |
15
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) ) |
17 |
13 1 3
|
grplid |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 0 + 𝑋 ) = 𝑋 ) |
18 |
12 16 17
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 0 + 𝑋 ) = 𝑋 ) |
19 |
18
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 = ( 0 + 𝑋 ) ) |
20 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) |
21 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑇 ∩ 𝑈 ) = { 0 } ) |
22 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) |
23 |
2
|
lsmub2 |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
24 |
5 6 23
|
syl2anc |
⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
25 |
24
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) |
26 |
3
|
subg0cl |
⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑇 ) |
27 |
10 26
|
syl |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 0 ∈ 𝑇 ) |
28 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 ) |
29 |
1 2 3 4 10 20 21 22 9 25 27 28
|
pj1eq |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 = ( 0 + 𝑋 ) ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 0 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 𝑋 ) ) ) |
30 |
19 29
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 0 ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑋 ) = 𝑋 ) ) |
31 |
30
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑋 ) = 0 ) |