Metamath Proof Explorer

Theorem symg2bas

Description: The symmetric group on a pair is the symmetric group S_2 consisting of the identity and the transposition. Notice that this statement is valid for proper pairs only. In the case that both elements are identical, i.e., the pairs are actually singletons, this theorem would be about S_1, see Theorem symg1bas . (Contributed by AV, 9-Dec-2018) (Proof shortened by AV, 16-Jun-2022)

Ref Expression
Hypotheses symg1bas.1 
|- G = ( SymGrp ` A )
symg1bas.2 
|- B = ( Base ` G )
symg2bas.0 
|- A = { I , J }
Assertion symg2bas 
|- ( ( I e. V /\ J e. W ) -> B = { { <. I , I >. , <. J , J >. } , { <. I , J >. , <. J , I >. } } )

Proof

Step Hyp Ref Expression
1 symg1bas.1 
 |-  G = ( SymGrp ` A )
2 symg1bas.2 
 |-  B = ( Base ` G )
3 symg2bas.0 
 |-  A = { I , J }
4 eqid 
 |-  ( SymGrp ` { J } ) = ( SymGrp ` { J } )
5 eqid 
 |-  ( Base ` ( SymGrp ` { J } ) ) = ( Base ` ( SymGrp ` { J } ) )
6 eqid 
 |-  { J } = { J }
7 4 5 6 symg1bas 
 |-  ( J e. W -> ( Base ` ( SymGrp ` { J } ) ) = { { <. J , J >. } } )
8 7 ad2antll 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> ( Base ` ( SymGrp ` { J } ) ) = { { <. J , J >. } } )
9 df-pr 
 |-  { I , J } = ( { I } u. { J } )
10 sneq 
 |-  ( I = J -> { I } = { J } )
11 10 uneq1d 
 |-  ( I = J -> ( { I } u. { J } ) = ( { J } u. { J } ) )
12 11 adantr 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> ( { I } u. { J } ) = ( { J } u. { J } ) )
13 unidm 
 |-  ( { J } u. { J } ) = { J }
14 12 13 eqtrdi 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> ( { I } u. { J } ) = { J } )
15 9 14 eqtrid 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> { I , J } = { J } )
16 3 15 eqtrid 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> A = { J } )
17 16 fveq2d 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> ( SymGrp ` A ) = ( SymGrp ` { J } ) )
18 1 17 eqtrid 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> G = ( SymGrp ` { J } ) )
19 18 fveq2d 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> ( Base ` G ) = ( Base ` ( SymGrp ` { J } ) ) )
20 2 19 eqtrid 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> B = ( Base ` ( SymGrp ` { J } ) ) )
21 id 
 |-  ( I = J -> I = J )
22 21 21 opeq12d 
 |-  ( I = J -> <. I , I >. = <. J , J >. )
23 22 adantr 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> <. I , I >. = <. J , J >. )
24 23 preq1d 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> { <. I , I >. , <. J , J >. } = { <. J , J >. , <. J , J >. } )
25 eqid 
 |-  <. J , J >. = <. J , J >.
26 opex 
 |-  <. J , J >. e. _V
27 26 26 preqsn 
 |-  ( { <. J , J >. , <. J , J >. } = { <. J , J >. } <-> ( <. J , J >. = <. J , J >. /\ <. J , J >. = <. J , J >. ) )
28 25 25 27 mpbir2an 
 |-  { <. J , J >. , <. J , J >. } = { <. J , J >. }
29 24 28 eqtrdi 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> { <. I , I >. , <. J , J >. } = { <. J , J >. } )
30 opeq1 
 |-  ( I = J -> <. I , J >. = <. J , J >. )
31 opeq2 
 |-  ( I = J -> <. J , I >. = <. J , J >. )
32 30 31 preq12d 
 |-  ( I = J -> { <. I , J >. , <. J , I >. } = { <. J , J >. , <. J , J >. } )
33 32 28 eqtrdi 
 |-  ( I = J -> { <. I , J >. , <. J , I >. } = { <. J , J >. } )
34 33 adantr 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> { <. I , J >. , <. J , I >. } = { <. J , J >. } )
35 29 34 preq12d 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> { { <. I , I >. , <. J , J >. } , { <. I , J >. , <. J , I >. } } = { { <. J , J >. } , { <. J , J >. } } )
36 eqid 
 |-  { <. J , J >. } = { <. J , J >. }
37 snex 
 |-  { <. J , J >. } e. _V
38 37 37 preqsn 
 |-  ( { { <. J , J >. } , { <. J , J >. } } = { { <. J , J >. } } <-> ( { <. J , J >. } = { <. J , J >. } /\ { <. J , J >. } = { <. J , J >. } ) )
39 36 36 38 mpbir2an 
 |-  { { <. J , J >. } , { <. J , J >. } } = { { <. J , J >. } }
40 35 39 eqtrdi 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> { { <. I , I >. , <. J , J >. } , { <. I , J >. , <. J , I >. } } = { { <. J , J >. } } )
41 8 20 40 3eqtr4d 
 |-  ( ( I = J /\ ( I e. V /\ J e. W ) ) -> B = { { <. I , I >. , <. J , J >. } , { <. I , J >. , <. J , I >. } } )
42 2 fvexi 
 |-  B e. _V
43 42 a1i 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> B e. _V )
44 neqne 
 |-  ( -. I = J -> I =/= J )
45 44 anim2i 
 |-  ( ( ( I e. V /\ J e. W ) /\ -. I = J ) -> ( ( I e. V /\ J e. W ) /\ I =/= J ) )
46 df-3an 
 |-  ( ( I e. V /\ J e. W /\ I =/= J ) <-> ( ( I e. V /\ J e. W ) /\ I =/= J ) )
47 45 46 sylibr 
 |-  ( ( ( I e. V /\ J e. W ) /\ -. I = J ) -> ( I e. V /\ J e. W /\ I =/= J ) )
48 47 ancoms 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> ( I e. V /\ J e. W /\ I =/= J ) )
49 1 2 3 symg2hash 
 |-  ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` B ) = 2 )
50 48 49 syl 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> ( # ` B ) = 2 )
51 id 
 |-  ( I e. V -> I e. V )
52 51 ancri 
 |-  ( I e. V -> ( I e. V /\ I e. V ) )
53 id 
 |-  ( J e. W -> J e. W )
54 53 ancri 
 |-  ( J e. W -> ( J e. W /\ J e. W ) )
55 52 54 anim12i 
 |-  ( ( I e. V /\ J e. W ) -> ( ( I e. V /\ I e. V ) /\ ( J e. W /\ J e. W ) ) )
56 df-ne 
 |-  ( I =/= J <-> -. I = J )
57 id 
 |-  ( I =/= J -> I =/= J )
58 57 ancri 
 |-  ( I =/= J -> ( I =/= J /\ I =/= J ) )
59 56 58 sylbir 
 |-  ( -. I = J -> ( I =/= J /\ I =/= J ) )
60 f1oprg 
 |-  ( ( ( I e. V /\ I e. V ) /\ ( J e. W /\ J e. W ) ) -> ( ( I =/= J /\ I =/= J ) -> { <. I , I >. , <. J , J >. } : { I , J } -1-1-onto-> { I , J } ) )
61 60 imp 
 |-  ( ( ( ( I e. V /\ I e. V ) /\ ( J e. W /\ J e. W ) ) /\ ( I =/= J /\ I =/= J ) ) -> { <. I , I >. , <. J , J >. } : { I , J } -1-1-onto-> { I , J } )
62 55 59 61 syl2anr 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> { <. I , I >. , <. J , J >. } : { I , J } -1-1-onto-> { I , J } )
63 eqidd 
 |-  ( A = { I , J } -> { <. I , I >. , <. J , J >. } = { <. I , I >. , <. J , J >. } )
64 id 
 |-  ( A = { I , J } -> A = { I , J } )
65 63 64 64 f1oeq123d 
 |-  ( A = { I , J } -> ( { <. I , I >. , <. J , J >. } : A -1-1-onto-> A <-> { <. I , I >. , <. J , J >. } : { I , J } -1-1-onto-> { I , J } ) )
66 3 65 ax-mp 
 |-  ( { <. I , I >. , <. J , J >. } : A -1-1-onto-> A <-> { <. I , I >. , <. J , J >. } : { I , J } -1-1-onto-> { I , J } )
67 62 66 sylibr 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> { <. I , I >. , <. J , J >. } : A -1-1-onto-> A )
68 prex 
 |-  { <. I , I >. , <. J , J >. } e. _V
69 1 2 elsymgbas2 
 |-  ( { <. I , I >. , <. J , J >. } e. _V -> ( { <. I , I >. , <. J , J >. } e. B <-> { <. I , I >. , <. J , J >. } : A -1-1-onto-> A ) )
70 68 69 ax-mp 
 |-  ( { <. I , I >. , <. J , J >. } e. B <-> { <. I , I >. , <. J , J >. } : A -1-1-onto-> A )
71 67 70 sylibr 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> { <. I , I >. , <. J , J >. } e. B )
72 f1oprswap 
 |-  ( ( I e. V /\ J e. W ) -> { <. I , J >. , <. J , I >. } : { I , J } -1-1-onto-> { I , J } )
73 eqidd 
 |-  ( A = { I , J } -> { <. I , J >. , <. J , I >. } = { <. I , J >. , <. J , I >. } )
74 73 64 64 f1oeq123d 
 |-  ( A = { I , J } -> ( { <. I , J >. , <. J , I >. } : A -1-1-onto-> A <-> { <. I , J >. , <. J , I >. } : { I , J } -1-1-onto-> { I , J } ) )
75 3 74 ax-mp 
 |-  ( { <. I , J >. , <. J , I >. } : A -1-1-onto-> A <-> { <. I , J >. , <. J , I >. } : { I , J } -1-1-onto-> { I , J } )
76 72 75 sylibr 
 |-  ( ( I e. V /\ J e. W ) -> { <. I , J >. , <. J , I >. } : A -1-1-onto-> A )
77 76 adantl 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> { <. I , J >. , <. J , I >. } : A -1-1-onto-> A )
78 prex 
 |-  { <. I , J >. , <. J , I >. } e. _V
79 1 2 elsymgbas2 
 |-  ( { <. I , J >. , <. J , I >. } e. _V -> ( { <. I , J >. , <. J , I >. } e. B <-> { <. I , J >. , <. J , I >. } : A -1-1-onto-> A ) )
80 78 79 ax-mp 
 |-  ( { <. I , J >. , <. J , I >. } e. B <-> { <. I , J >. , <. J , I >. } : A -1-1-onto-> A )
81 77 80 sylibr 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> { <. I , J >. , <. J , I >. } e. B )
82 opex 
 |-  <. I , I >. e. _V
83 82 26 pm3.2i 
 |-  ( <. I , I >. e. _V /\ <. J , J >. e. _V )
84 opex 
 |-  <. I , J >. e. _V
85 opex 
 |-  <. J , I >. e. _V
86 84 85 pm3.2i 
 |-  ( <. I , J >. e. _V /\ <. J , I >. e. _V )
87 83 86 pm3.2i 
 |-  ( ( <. I , I >. e. _V /\ <. J , J >. e. _V ) /\ ( <. I , J >. e. _V /\ <. J , I >. e. _V ) )
88 opthg2 
 |-  ( ( I e. V /\ J e. W ) -> ( <. I , I >. = <. I , J >. <-> ( I = I /\ I = J ) ) )
89 eqtr 
 |-  ( ( I = I /\ I = J ) -> I = J )
90 88 89 syl6bi 
 |-  ( ( I e. V /\ J e. W ) -> ( <. I , I >. = <. I , J >. -> I = J ) )
91 90 necon3d 
 |-  ( ( I e. V /\ J e. W ) -> ( I =/= J -> <. I , I >. =/= <. I , J >. ) )
92 91 com12 
 |-  ( I =/= J -> ( ( I e. V /\ J e. W ) -> <. I , I >. =/= <. I , J >. ) )
93 56 92 sylbir 
 |-  ( -. I = J -> ( ( I e. V /\ J e. W ) -> <. I , I >. =/= <. I , J >. ) )
94 93 imp 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> <. I , I >. =/= <. I , J >. )
95 52 adantr 
 |-  ( ( I e. V /\ J e. W ) -> ( I e. V /\ I e. V ) )
96 opthg 
 |-  ( ( I e. V /\ I e. V ) -> ( <. I , I >. = <. J , I >. <-> ( I = J /\ I = I ) ) )
97 95 96 syl 
 |-  ( ( I e. V /\ J e. W ) -> ( <. I , I >. = <. J , I >. <-> ( I = J /\ I = I ) ) )
98 simpl 
 |-  ( ( I = J /\ I = I ) -> I = J )
99 97 98 syl6bi 
 |-  ( ( I e. V /\ J e. W ) -> ( <. I , I >. = <. J , I >. -> I = J ) )
100 99 necon3d 
 |-  ( ( I e. V /\ J e. W ) -> ( I =/= J -> <. I , I >. =/= <. J , I >. ) )
101 100 com12 
 |-  ( I =/= J -> ( ( I e. V /\ J e. W ) -> <. I , I >. =/= <. J , I >. ) )
102 56 101 sylbir 
 |-  ( -. I = J -> ( ( I e. V /\ J e. W ) -> <. I , I >. =/= <. J , I >. ) )
103 102 imp 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> <. I , I >. =/= <. J , I >. )
104 94 103 jca 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> ( <. I , I >. =/= <. I , J >. /\ <. I , I >. =/= <. J , I >. ) )
105 104 orcd 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> ( ( <. I , I >. =/= <. I , J >. /\ <. I , I >. =/= <. J , I >. ) \/ ( <. J , J >. =/= <. I , J >. /\ <. J , J >. =/= <. J , I >. ) ) )
106 prneimg 
 |-  ( ( ( <. I , I >. e. _V /\ <. J , J >. e. _V ) /\ ( <. I , J >. e. _V /\ <. J , I >. e. _V ) ) -> ( ( ( <. I , I >. =/= <. I , J >. /\ <. I , I >. =/= <. J , I >. ) \/ ( <. J , J >. =/= <. I , J >. /\ <. J , J >. =/= <. J , I >. ) ) -> { <. I , I >. , <. J , J >. } =/= { <. I , J >. , <. J , I >. } ) )
107 87 105 106 mpsyl 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> { <. I , I >. , <. J , J >. } =/= { <. I , J >. , <. J , I >. } )
108 hash2prd 
 |-  ( ( B e. _V /\ ( # ` B ) = 2 ) -> ( ( { <. I , I >. , <. J , J >. } e. B /\ { <. I , J >. , <. J , I >. } e. B /\ { <. I , I >. , <. J , J >. } =/= { <. I , J >. , <. J , I >. } ) -> B = { { <. I , I >. , <. J , J >. } , { <. I , J >. , <. J , I >. } } ) )
109 108 imp 
 |-  ( ( ( B e. _V /\ ( # ` B ) = 2 ) /\ ( { <. I , I >. , <. J , J >. } e. B /\ { <. I , J >. , <. J , I >. } e. B /\ { <. I , I >. , <. J , J >. } =/= { <. I , J >. , <. J , I >. } ) ) -> B = { { <. I , I >. , <. J , J >. } , { <. I , J >. , <. J , I >. } } )
110 43 50 71 81 107 109 syl23anc 
 |-  ( ( -. I = J /\ ( I e. V /\ J e. W ) ) -> B = { { <. I , I >. , <. J , J >. } , { <. I , J >. , <. J , I >. } } )
111 41 110 pm2.61ian 
 |-  ( ( I e. V /\ J e. W ) -> B = { { <. I , I >. , <. J , J >. } , { <. I , J >. , <. J , I >. } } )